defpred S₁[ object , object ] means ex y being Element of F₁() st
( $1 = Class (F₃(),y) & $2 = Class (F₃(),F₂(y)) );
A2: for a being object st a in Class F₃() holds
ex b being object st
( b in Class F₃() & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in Class F₃() implies ex b being object st
( b in Class F₃() & S₁[a,b] ) )
assume a in Class F₃() ; :: thesis: ex b being object st
( b in Class F₃() & S₁[a,b] )
then consider c being object such that
A5: c in F₁() and
A6: a = Class (F₃(),c) by EQREL_1:def 3;
reconsider y = c as Element of F₁() by A5;
take b = Class (F₃(),F₂(y)); :: thesis: ( b in Class F₃() & S₁[a,b] )
thus b in Class F₃() by EQREL_1:def 3; :: thesis: S₁[a,b]
thus S₁[a,b] by A6; :: thesis: verum

end;

consider f being Function of (Class F₃()),(Class F₃()) such that
A10: for a being object st a in Class F₃() holds
S₁[a,f . a] from FUNCT_2:sch 1(A2);
take f ; :: thesis: for x being Element of F₁() holds f . (Class (F₃(),x)) = Class (F₃(),F₂(x))
let x be Element of F₁(); :: thesis: f . (Class (F₃(),x)) = Class (F₃(),F₂(x))
set u = Class (F₃(),x);
Class (F₃(),x) in Class F₃() by EQREL_1:def 3;
then S₁[ Class (F₃(),x),f . (Class (F₃(),x))] by A10;
then consider y being Element of F₁() such that
A11: Class (F₃(),x) = Class (F₃(),y) and
A12: f . (Class (F₃(),y)) = Class (F₃(),F₂(y)) ;
y in Class (F₃(),x) by A11, EQREL_1:23;
then [x,y] in F₃() by EQREL_1:18;
then [F₂(x),F₂(y)] in F₃() by A1;
then F₂(y) in Class (F₃(),F₂(x)) by EQREL_1:18;
hence f . (Class (F₃(),x)) = Class (F₃(),F₂(x)) by A11, A12, EQREL_1:23; :: thesis: verum