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:9;
hence x in Funcs (E,E) ; :: thesis: verum

end;

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

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:9; :: 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 that
A4: [x,y1] in h and
A5: [x,y2] in h ; :: thesis: y1 = y2
consider x9, y9 being set such that
x9 in O and
A6: ( y9 in {(id E)} & [x,y1] = [x9,y9] ) by A4, ZFMISC_1:def 2;
A7: ( y9 = id E & y1 = y9 ) by A6, TARSKI:def 1, ZFMISC_1:27;
consider x99, y99 being set such that
x99 in O and
A8: y99 in {(id E)} and
A9: [x,y2] = [x99,y99] by A5, ZFMISC_1:def 2;
y99 = id E by A8, TARSKI:def 1;
hence y1 = y2 by A9, A7, ZFMISC_1:27; :: 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