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

proof

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

end;

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