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

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
A3: x = [s,F₃(s)] ;
F₃(s) in Funcs F₁(),F₁() by FUNCT_2:12;
hence x in [:the carrier of F₂(),(Funcs F₁(),F₁()):] by A3, ZFMISC_1:def 2; :: thesis: verum

end;

then A4: { [s,F₃(s)] where s is Element of F₂() : verum } c= [:the carrier of F₂(),(Funcs F₁(),F₁()):] by TARSKI:def 3;

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)] ;
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
A6: [x,y2] = [s2,F₃(s2)] ;
( x = s1 & y1 = F₃(s1) & x = s2 & y2 = F₃(s2) ) by A5, A6, ZFMISC_1:33;
hence y1 = y2 ; :: 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 A4, FUNCT_1:def 1;
T is quasi_total

proof

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 A7: [x,y] in T ; :: thesis: x in the carrier of F₂()
consider s being Element of F₂() such that
A8: [x,y] = [s,F₃(s)] by A7;
x = s by A8, ZFMISC_1:33;
hence x in the carrier of F₂() ; :: thesis: verum

end;

then the carrier of F₂() = dom T by RELAT_1:def 4;
hence T is quasi_total by FUNCT_2:def 1; :: thesis: verum

end;

then reconsider T = T as Action of the carrier of F₂(),F₁() ;
A9: dom T = the carrier of F₂() by FUNCT_2:def 1;
then [(1_ F₂()),(T . (1_ F₂()))] in T by FUNCT_1:8;
then consider s' being Element of F₂() such that
A10: [(1_ F₂()),(T . (1_ F₂()))] = [s',F₃(s')] ;
A11: ( 1_ F₂() = s' & T . (1_ F₂()) = F₃(s') ) by A10, ZFMISC_1:33;

now

let s1, s2 be Element of F₂(); :: thesis: T ^ (s1 * s2) = (T ^ s1) * (T ^ s2)
( s1 in the carrier of F₂() & s2 in the carrier of F₂() & s1 * s2 in the carrier of F₂() ) ;
then ( s1 in dom T & s2 in dom T & s1 * s2 in dom T ) by FUNCT_2:def 1;
then A12: ( [s1,(T . s1)] in T & [s2,(T . s2)] in T & [(s1 * s2),(T . (s1 * s2))] in T ) by FUNCT_1:8;
then consider s1' being Element of F₂() such that
A13: [s1,(T . s1)] = [s1',F₃(s1')] ;
consider s2' being Element of F₂() such that
A14: [s2,(T . s2)] = [s2',F₃(s2')] by A12;
consider s12' being Element of F₂() such that
A15: [(s1 * s2),(T . (s1 * s2))] = [s12',F₃(s12')] by A12;
A16: ( s1 = s1' & F₃(s1') = T . s1 ) by A13, ZFMISC_1:33;
A17: ( s2 = s2' & F₃(s2') = T . s2 ) by A14, ZFMISC_1:33;
thus T ^ (s1 * s2) = F₃(s12') by A15, ZFMISC_1:33
.= F₃((s1 * s2)) by A15, ZFMISC_1:33
.= (T ^ s1) * (T ^ s2) by A2, A16, A17 ; :: thesis: verum

end;

then reconsider T = T as LeftOperation of F₂(),F₁() by A1, A11, 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 A9, FUNCT_1:8;
then consider s' being Element of F₂() such that
A18: [s,(T . s)] = [s',F₃(s')] ;
( s = s' & T . s = F₃(s') ) by A18, ZFMISC_1:33;
hence T . s = F₃(s) ; :: thesis: verum

end;