let a be Domain-Sequence; :: thesis: for b being BinOps of a
for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
let b be BinOps of a; :: thesis: for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
let u be UnOps of a; :: thesis: ( ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) implies Frege u is_an_inverseOp_wrt [:b:] )
assume A1: for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ; :: thesis: Frege u is_an_inverseOp_wrt [:b:]
defpred S₁[ object , object ] means ex i being Element of dom a st
( $1 = i & $2 = the_unity_wrt (b . i) );
A2: for x being object st x in dom a holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom a implies ex y being object st S₁[x,y] )
assume x in dom a ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as Element of dom a ;
take the_unity_wrt (b . i) ; :: thesis: S₁[x, the_unity_wrt (b . i)]
thus S₁[x, the_unity_wrt (b . i)] ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = dom a & ( for x being object st x in dom a holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);

now :: thesis: for x being object st x in dom a holds
f . x in a . x

let x be object ; :: thesis: ( x in dom a implies f . x in a . x )
assume x in dom a ; :: thesis: f . x in a . x
then ex i being Element of dom a st
( x = i & f . x = the_unity_wrt (b . i) ) by A3;
hence f . x in a . x ; :: thesis: verum

end;

then reconsider f = f as Element of product a by A3, CARD_3:9;
let x be Element of product a; :: according to FINSEQOP:def 1 :: thesis: ( [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] & [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] )

A5: now :: thesis: for y being object st y in dom a holds
([:b:] . (x,((Frege u) . x))) . y = f . y

let y be object ; :: thesis: ( y in dom a implies ([:b:] . (x,((Frege u) . x))) . y = f . y )
assume y in dom a ; :: thesis: ([:b:] . (x,((Frege u) . x))) . y = f . y
then reconsider i = y as Element of dom a ;
A6: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (x,((Frege u) . x))) . i = (b . i) . ((x . i),(((Frege u) . x) . i)) ) by A3, Def8;
hence ([:b:] . (x,((Frege u) . x))) . y = f . y by A6; :: thesis: verum

end;

now :: thesis: for i being Element of dom a holds f . i is_a_unity_wrt b . i

let i be Element of dom a; :: thesis: f . i is_a_unity_wrt b . i
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & b . i is having_a_unity ) by A1, A3;
hence f . i is_a_unity_wrt b . i by SETWISEO:14; :: thesis: verum

end;

then f is_a_unity_wrt [:b:] by Th19;
then A7: f = the_unity_wrt [:b:] by BINOP_1:def 8;

A8: now :: thesis: for y being object st y in dom a holds
([:b:] . (((Frege u) . x),x)) . y = f . y

let y be object ; :: thesis: ( y in dom a implies ([:b:] . (((Frege u) . x),x)) . y = f . y )
assume y in dom a ; :: thesis: ([:b:] . (((Frege u) . x),x)) . y = f . y
then reconsider i = y as Element of dom a ;
A9: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (((Frege u) . x),x)) . i = (b . i) . ((((Frege u) . x) . i),(x . i)) ) by A3, Def8;
hence ([:b:] . (((Frege u) . x),x)) . y = f . y by A9; :: thesis: verum

end;

dom ([:b:] . (x,((Frege u) . x))) = dom a by CARD_3:9;
hence [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] by A7, A5, CARD_3:9; :: thesis: [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:]
dom ([:b:] . (((Frege u) . x),x)) = dom a by CARD_3:9;
hence [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] by A7, A8, CARD_3:9; :: thesis: verum