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

set h = [:O,{(id E)}:];

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

h is Action of O,E by A1, FUNCT_2:def 1;

hence [:O,{(id E)}:] is Action of O,E ; :: thesis: verum

set h = [:O,{(id E)}:];

now :: thesis: for x being object st x in {(id E)} holds

x in Funcs (E,E)

then
{(id E)} c= Funcs (E,E)
;x in Funcs (E,E)

let x be object ; :: 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;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

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

A1: now :: thesis: ( ( ( Funcs (E,E) = {} implies O = {} ) implies O = dom h ) & ( O = {} implies h = {} ) )

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

hence h = {} ; :: thesis: verum

end;proof

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

end;now :: thesis: for x being object st x in O holds

ex y being object st [x,y] in h

hence
O = dom h
by RELSET_1:9; :: thesis: verumex y being object st [x,y] in h

let x be object ; :: thesis: ( x in O implies ex y being object st [x,y] in h )

assume A2: x in O ; :: thesis: ex y being object st [x,y] in h

reconsider y = id E as object ;

take y = y; :: thesis: [x,y] in h

y in {(id E)} by TARSKI:def 1;

hence [x,y] in h by A2, ZFMISC_1:def 2; :: thesis: verum

end;assume A2: x in O ; :: thesis: ex y being object st [x,y] in h

reconsider y = id E as object ;

take y = y; :: thesis: [x,y] in h

y in {(id E)} by TARSKI:def 1;

hence [x,y] in h by A2, ZFMISC_1:def 2; :: thesis: verum

hence h = {} ; :: thesis: verum

now :: thesis: for x, y1, y2 being object st [x,y1] in h & [x,y2] in h holds

y1 = y2

then reconsider h = h as PartFunc of O,(Funcs (E,E)) by FUNCT_1:def 1;y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in h & [x,y2] in h implies y1 = y2 )

assume that

A3: [x,y1] in h and

A4: [x,y2] in h ; :: thesis: y1 = y2

consider x9, y9 being object such that

x9 in O and

A5: ( y9 in {(id E)} & [x,y1] = [x9,y9] ) by A3, ZFMISC_1:def 2;

A6: ( y9 = id E & y1 = y9 ) by A5, TARSKI:def 1, XTUPLE_0:1;

consider x99, y99 being object such that

x99 in O and

A7: y99 in {(id E)} and

A8: [x,y2] = [x99,y99] by A4, ZFMISC_1:def 2;

y99 = id E by A7, TARSKI:def 1;

hence y1 = y2 by A8, A6, XTUPLE_0:1; :: thesis: verum

end;assume that

A3: [x,y1] in h and

A4: [x,y2] in h ; :: thesis: y1 = y2

consider x9, y9 being object such that

x9 in O and

A5: ( y9 in {(id E)} & [x,y1] = [x9,y9] ) by A3, ZFMISC_1:def 2;

A6: ( y9 = id E & y1 = y9 ) by A5, TARSKI:def 1, XTUPLE_0:1;

consider x99, y99 being object such that

x99 in O and

A7: y99 in {(id E)} and

A8: [x,y2] = [x99,y99] by A4, ZFMISC_1:def 2;

y99 = id E by A7, TARSKI:def 1;

hence y1 = y2 by A8, A6, XTUPLE_0:1; :: thesis: verum

h is Action of O,E by A1, FUNCT_2:def 1;

hence [:O,{(id E)}:] is Action of O,E ; :: thesis: verum