let O, E be set ; :: thesis: [:O,{(id E)}:] is Action of O,E
set h = [:O,{(id E)}:];

now

let x be set ; :: thesis: ( x in {(id E)} implies x in Funcs E,E )
assume x in {(id E)} ; :: thesis: x in Funcs E,E
then reconsider f = x as Function of E,E by TARSKI:def 1;
f in Funcs E,E by FUNCT_2:12;
hence x in Funcs E,E ; :: thesis: verum

end;

then {(id E)} c= Funcs E,E by TARSKI:def 3;
then [:O,{(id E)}:] c= [:O,(Funcs E,E):] by ZFMISC_1:118;
then reconsider h = [:O,{(id E)}:] as Relation of O,(Funcs E,E) ;

A1: now

thus ( ( Funcs E,E = {} implies O = {} ) implies O = dom h ) :: thesis: ( O = {} implies h = {} )

proof

assume ( Funcs E,E = {} implies O = {} ) ; :: thesis: O = dom h

now

let x be set ; :: thesis: ( x in O implies ex y being set st [x,y] in h )
assume A2: x in O ; :: thesis: ex y being set st [x,y] in h
consider y being set such that
A3: y = id E ;
take y = y; :: thesis: [x,y] in h
y in {(id E)} by A3, TARSKI:def 1;
hence [x,y] in h by A2, ZFMISC_1:def 2; :: thesis: verum

end;

hence O = dom h by RELSET_1:22; :: thesis: verum

end;

assume O = {} ; :: thesis: h = {}
hence h = {} ; :: thesis: verum

end;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in h & [x,y2] in h implies y1 = y2 )
assume A4: ( [x,y1] in h & [x,y2] in h ) ; :: thesis: y1 = y2
then consider x', y' being set such that
A5: ( x' in O & y' in {(id E)} & [x,y1] = [x',y'] ) by ZFMISC_1:def 2;
consider x'', y'' being set such that
A6: ( x'' in O & y'' in {(id E)} & [x,y2] = [x'',y''] ) by A4, ZFMISC_1:def 2;
A7: ( y' = id E & y'' = id E ) by A5, A6, TARSKI:def 1;
( y1 = y' & y2 = y'' ) by A5, A6, ZFMISC_1:33;
hence y1 = y2 by A7; :: thesis: verum

end;

then reconsider h = h as PartFunc of O,(Funcs E,E) by FUNCT_1:def 1;
h is Action of O,E by A1, FUNCT_2:def 1;
hence [:O,{(id E)}:] is Action of O,E ; :: thesis: verum