let O, E be set ; :: thesis: [:O,{(id E)}:] is Action of O,E
set h = [:O,{(id E)}:];
now :: thesis: for x being object st x in {(id E)} holds
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;
then {(id E)} c= Funcs (E,E) ;
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 = {} )
proof
assume ( Funcs (E,E) = {} implies O = {} ) ; :: thesis: O = dom h
now :: thesis: for x being object st x in O holds
ex 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;
hence O = dom h by RELSET_1:9; :: thesis: verum
end;
assume O = {} ; :: thesis: h = {}
hence h = {} ; :: thesis: verum
end;
now :: thesis: for x, y1, y2 being object st [x,y1] in h & [x,y2] in h holds
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;
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