set T = { [s,F₃(s)] where s is Element of F₂() : verum } ;

A3: now

let x be set ; :: thesis: ( x in { [s,F₃(s)] where s is Element of F₂() : verum } implies x in [: the carrier of F₂(),(Funcs (F₁(),F₁())):] )
assume x in { [s,F₃(s)] where s is Element of F₂() : verum } ; :: thesis: x in [: the carrier of F₂(),(Funcs (F₁(),F₁())):]
then consider s being Element of F₂() such that
A4: x = [s,F₃(s)] ;
F₃(s) in Funcs (F₁(),F₁()) by FUNCT_2:9;
hence x in [: the carrier of F₂(),(Funcs (F₁(),F₁())):] by A4, ZFMISC_1:def 2; :: thesis: verum

end;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [s,F₃(s)] where s is Element of F₂() : verum } & [x,y2] in { [s,F₃(s)] where s is Element of F₂() : verum } implies y1 = y2 )
assume [x,y1] in { [s,F₃(s)] where s is Element of F₂() : verum } ; :: thesis: ( [x,y2] in { [s,F₃(s)] where s is Element of F₂() : verum } implies y1 = y2 )
then consider s1 being Element of F₂() such that
A5: [x,y1] = [s1,F₃(s1)] ;
A6: x = s1 by A5, ZFMISC_1:27;
assume [x,y2] in { [s,F₃(s)] where s is Element of F₂() : verum } ; :: thesis: y1 = y2
then consider s2 being Element of F₂() such that
A7: [x,y2] = [s2,F₃(s2)] ;
x = s2 by A7, ZFMISC_1:27;
hence y1 = y2 by A5, A7, A6, ZFMISC_1:27; :: thesis: verum

end;

then reconsider T = { [s,F₃(s)] where s is Element of F₂() : verum } as Function-like Relation of the carrier of F₂(),(Funcs (F₁(),F₁())) by A3, FUNCT_1:def 1, TARSKI:def 3;

now

let x be set ; :: thesis: ( ( x in the carrier of F₂() implies ex y being set st [x,y] in T ) & ( ex y being set st [x,y] in T implies x in the carrier of F₂() ) )

hereby :: thesis: ( ex y being set st [x,y] in T implies x in the carrier of F₂() )

assume x in the carrier of F₂() ; :: thesis: ex y being set st [x,y] in T
then reconsider s = x as Element of F₂() ;
reconsider y = F₃(s) as set ;
take y = y; :: thesis: [x,y] in T
thus [x,y] in T ; :: thesis: verum

end;

given y being set such that A8: [x,y] in T ; :: thesis: x in the carrier of F₂()
consider s being Element of F₂() such that
A9: [x,y] = [s,F₃(s)] by A8;
x = s by A9, ZFMISC_1:27;
hence x in the carrier of F₂() ; :: thesis: verum

end;

then the carrier of F₂() = dom T by RELAT_1:def 4;
then reconsider T = T as Action of the carrier of F₂(),F₁() by FUNCT_2:def 1;

A10: now

let s1, s2 be Element of F₂(); :: thesis: T ^ (s1 * s2) = (T ^ s1) * (T ^ s2)
s1 in the carrier of F₂() ;
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 F₂() such that
A11: [s1,(T . s1)] = [s19,F₃(s19)] ;
A12: ( s1 = s19 & F₃(s19) = T . s1 ) by A11, ZFMISC_1:27;
s2 in the carrier of F₂() ;
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 F₂() such that
A13: [s2,(T . s2)] = [s29,F₃(s29)] ;
s1 * s2 in the carrier of F₂() ;
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 F₂() such that
A14: [(s1 * s2),(T . (s1 * s2))] = [s129,F₃(s129)] ;
A15: ( s2 = s29 & F₃(s29) = T . s2 ) by A13, ZFMISC_1:27;
thus T ^ (s1 * s2) = F₃(s129) by A14, ZFMISC_1:27
.= F₃((s1 * s2)) by A14, ZFMISC_1:27
.= (T ^ s1) * (T ^ s2) by A2, A12, A15 ; :: thesis: verum

end;

A16: dom T = the carrier of F₂() by FUNCT_2:def 1;
then [(1_ F₂()),(T . (1_ F₂()))] in T by FUNCT_1:1;
then consider s9 being Element of F₂() such that
A17: [(1_ F₂()),(T . (1_ F₂()))] = [s9,F₃(s9)] ;
( 1_ F₂() = s9 & T . (1_ F₂()) = F₃(s9) ) by A17, ZFMISC_1:27;
then reconsider T = T as LeftOperation of F₂(),F₁() by A1, A10, Def1;
take T ; :: thesis: for s being Element of F₂() holds T . s = F₃(s)
thus for s being Element of F₂() holds T . s = F₃(s) :: thesis: verum

proof

let s be Element of F₂(); :: thesis: T . s = F₃(s)
[s,(T . s)] in T by A16, FUNCT_1:1;
then consider s9 being Element of F₂() such that
A18: [s,(T . s)] = [s9,F₃(s9)] ;
s = s9 by A18, ZFMISC_1:27;
hence T . s = F₃(s) by A18, ZFMISC_1:27; :: thesis: verum

end;