defpred S1[ object , object , object ] means ex x, y being Element of F1() st
( $1 = Class (F3(),x) & $2 = Class (F3(),y) & $3 = Class (F3(),F2(x,y)) );
A2:
for a, b being object st a in Class F3() & b in Class F3() holds
ex c being object st
( c in Class F3() & S1[a,b,c] )
proof
let a,
b be
object ;
( a in Class F3() & b in Class F3() implies ex c being object st
( c in Class F3() & S1[a,b,c] ) )
assume that A3:
a in Class F3()
and A4:
b in Class F3()
;
ex c being object st
( c in Class F3() & S1[a,b,c] )
consider a1 being
object such that A5:
a1 in F1()
and A6:
a = Class (
F3(),
a1)
by A3, EQREL_1:def 3;
consider b1 being
object such that A7:
b1 in F1()
and A8:
b = Class (
F3(),
b1)
by A4, EQREL_1:def 3;
reconsider a1 =
a1,
b1 =
b1 as
Element of
F1()
by A5, A7;
take c =
Class (
F3(),
F2(
a1,
b1));
( c in Class F3() & S1[a,b,c] )
thus
c in Class F3()
by EQREL_1:def 3;
S1[a,b,c]
thus
S1[
a,
b,
c]
by A6, A8;
verum
end;
consider f being Function of [:(Class F3()),(Class F3()):],(Class F3()) such that
A10:
for a, b being object st a in Class F3() & b in Class F3() holds
S1[a,b,f . (a,b)]
from BINOP_1:sch 1(A2);
take
f
; for x, y being Element of F1() holds f . ((Class (F3(),x)),(Class (F3(),y))) = Class (F3(),F2(x,y))
let x, y be Element of F1(); f . ((Class (F3(),x)),(Class (F3(),y))) = Class (F3(),F2(x,y))
set u = Class (F3(),x);
set v = Class (F3(),y);
( Class (F3(),x) in Class F3() & Class (F3(),y) in Class F3() )
by EQREL_1:def 3;
then
S1[ Class (F3(),x), Class (F3(),y),f . ((Class (F3(),x)),(Class (F3(),y)))]
by A10;
then consider x1, y1 being Element of F1() such that
A11:
Class (F3(),x) = Class (F3(),x1)
and
A12:
Class (F3(),y) = Class (F3(),y1)
and
A13:
f . ((Class (F3(),x1)),(Class (F3(),y1))) = Class (F3(),F2(x1,y1))
;
( x1 in Class (F3(),x) & y1 in Class (F3(),y) )
by A11, A12, EQREL_1:23;
then
( [x,x1] in F3() & [y,y1] in F3() )
by EQREL_1:18;
then
[F2(x,y),F2(x1,y1)] in F3()
by A1;
then
F2(x1,y1) in Class (F3(),F2(x,y))
by EQREL_1:18;
hence
f . ((Class (F3(),x)),(Class (F3(),y))) = Class (F3(),F2(x,y))
by A11, A12, A13, EQREL_1:23; verum