set T = { [s,F3(s)] where s is Element of F2() : verum } ;
A3: now :: thesis: for x being object st x in { [s,F3(s)] where s is Element of F2() : verum } holds
x in [: the carrier of F2(),(Funcs (F1(),F1())):]
let x be object ; :: thesis: ( x in { [s,F3(s)] where s is Element of F2() : verum } implies x in [: the carrier of F2(),(Funcs (F1(),F1())):] )
assume x in { [s,F3(s)] where s is Element of F2() : verum } ; :: thesis: x in [: the carrier of F2(),(Funcs (F1(),F1())):]
then consider s being Element of F2() such that
A4: x = [s,F3(s)] ;
F3(s) in Funcs (F1(),F1()) by FUNCT_2:9;
hence x in [: the carrier of F2(),(Funcs (F1(),F1())):] by A4, ZFMISC_1:def 2; :: thesis: verum
end;
now :: thesis: for x, y1, y2 being object st [x,y1] in { [s,F3(s)] where s is Element of F2() : verum } & [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [s,F3(s)] where s is Element of F2() : verum } & [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } implies y1 = y2 )
assume [x,y1] in { [s,F3(s)] where s is Element of F2() : verum } ; :: thesis: ( [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } implies y1 = y2 )
then consider s1 being Element of F2() such that
A5: [x,y1] = [s1,F3(s1)] ;
A6: x = s1 by A5, XTUPLE_0:1;
assume [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } ; :: thesis: y1 = y2
then consider s2 being Element of F2() such that
A7: [x,y2] = [s2,F3(s2)] ;
x = s2 by A7, XTUPLE_0:1;
hence y1 = y2 by A5, A7, A6, XTUPLE_0:1; :: thesis: verum
end;
then reconsider T = { [s,F3(s)] where s is Element of F2() : verum } as Function-like Relation of the carrier of F2(),(Funcs (F1(),F1())) by A3, FUNCT_1:def 1, TARSKI:def 3;
now :: thesis: for x being object holds
( ( x in the carrier of F2() implies ex y being object st [x,y] in T ) & ( ex y being object st [x,y] in T implies x in the carrier of F2() ) )
let x be object ; :: thesis: ( ( x in the carrier of F2() implies ex y being object st [x,y] in T ) & ( ex y being object st [x,y] in T implies x in the carrier of F2() ) )
hereby :: thesis: ( ex y being object st [x,y] in T implies x in the carrier of F2() )
assume x in the carrier of F2() ; :: thesis: ex y being object st [x,y] in T
then reconsider s = x as Element of F2() ;
reconsider y = F3(s) as object ;
take y = y; :: thesis: [x,y] in T
thus [x,y] in T ; :: thesis: verum
end;
given y being object such that A8: [x,y] in T ; :: thesis: x in the carrier of F2()
consider s being Element of F2() such that
A9: [x,y] = [s,F3(s)] by A8;
x = s by A9, XTUPLE_0:1;
hence x in the carrier of F2() ; :: thesis: verum
end;
then the carrier of F2() = dom T by XTUPLE_0:def 12;
then reconsider T = T as Action of the carrier of F2(),F1() by FUNCT_2:def 1;
A10: now :: thesis: for s1, s2 being Element of F2() holds T ^ (s1 * s2) = (T ^ s1) * (T ^ s2)
let s1, s2 be Element of F2(); :: thesis: T ^ (s1 * s2) = (T ^ s1) * (T ^ s2)
s1 in the carrier of F2() ;
then s1 in dom T by FUNCT_2:def 1;
then [s1,(T . s1)] in T by FUNCT_1:1;
then consider s19 being Element of F2() such that
A11: [s1,(T . s1)] = [s19,F3(s19)] ;
A12: ( s1 = s19 & F3(s19) = T . s1 ) by A11, XTUPLE_0:1;
s2 in the carrier of F2() ;
then s2 in dom T by FUNCT_2:def 1;
then [s2,(T . s2)] in T by FUNCT_1:1;
then consider s29 being Element of F2() such that
A13: [s2,(T . s2)] = [s29,F3(s29)] ;
s1 * s2 in the carrier of F2() ;
then s1 * s2 in dom T by FUNCT_2:def 1;
then [(s1 * s2),(T . (s1 * s2))] in T by FUNCT_1:1;
then consider s129 being Element of F2() such that
A14: [(s1 * s2),(T . (s1 * s2))] = [s129,F3(s129)] ;
A15: ( s2 = s29 & F3(s29) = T . s2 ) by A13, XTUPLE_0:1;
thus T ^ (s1 * s2) = F3(s129) by A14, XTUPLE_0:1
.= F3((s1 * s2)) by A14, XTUPLE_0:1
.= (T ^ s1) * (T ^ s2) by A2, A12, A15 ; :: thesis: verum
end;
A16: dom T = the carrier of F2() by FUNCT_2:def 1;
then [(1_ F2()),(T . (1_ F2()))] in T by FUNCT_1:1;
then consider s9 being Element of F2() such that
A17: [(1_ F2()),(T . (1_ F2()))] = [s9,F3(s9)] ;
( 1_ F2() = s9 & T . (1_ F2()) = F3(s9) ) by A17, XTUPLE_0:1;
then reconsider T = T as LeftOperation of F2(),F1() by A1, A10, Def1;
take T ; :: thesis: for s being Element of F2() holds T . s = F3(s)
thus for s being Element of F2() holds T . s = F3(s) :: thesis: verum
proof
let s be Element of F2(); :: thesis: T . s = F3(s)
[s,(T . s)] in T by A16, FUNCT_1:1;
then consider s9 being Element of F2() such that
A18: [s,(T . s)] = [s9,F3(s9)] ;
s = s9 by A18, XTUPLE_0:1;
hence T . s = F3(s) by A18, XTUPLE_0:1; :: thesis: verum
end;