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₁[ set , set ] means ex i being Element of dom a st
( $1 = i & $2 = the_unity_wrt (b . i) );
A2: for x being set st x in dom a holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in dom a implies ex y being set st S₁[x,y] )
assume x in dom a ; :: thesis: ex y being set 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
A4: ( dom f = dom a & ( for x being set st x in dom a holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);

now

let x be set ; :: 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 A4;
hence f . x in a . x ; :: thesis: verum

end;

then reconsider f = f as Element of product a by A4, CARD_3:18;

now

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) ) by A4;
then ( f . i = the_unity_wrt (b . i) & b . i is having_a_unity ) by A1;
hence f . i is_a_unity_wrt b . i by SETWISEO:22; :: thesis: verum

end;

then f is_a_unity_wrt [:b:] by Th27;
then A5: f = the_unity_wrt [:b:] by BINOP_1:def 8;
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:] )
A6: ( dom ([:b:] . x,((Frege u) . x)) = dom a & dom ([:b:] . ((Frege u) . x),x) = dom a & dom f = dom a ) by CARD_3:18;

now

let y be set ; :: 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 ;
ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) by A4;
then ( ([:b:] . x,((Frege u) . x)) . i = (b . i) . (x . i),(((Frege u) . x) . i) & ((Frege u) . x) . i = (u . i) . (x . i) & f . i = the_unity_wrt (b . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Def10, Th23;
hence ([:b:] . x,((Frege u) . x)) . y = f . y by FINSEQOP:def 1; :: thesis: verum

end;

hence [:b:] . x,((Frege u) . x) = the_unity_wrt [:b:] by A5, A6, FUNCT_1:9; :: thesis: [:b:] . ((Frege u) . x),x = the_unity_wrt [:b:]

now

let y be set ; :: 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 ;
ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) by A4;
then ( ([:b:] . ((Frege u) . x),x) . i = (b . i) . (((Frege u) . x) . i),(x . i) & ((Frege u) . x) . i = (u . i) . (x . i) & f . i = the_unity_wrt (b . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Def10, Th23;
hence ([:b:] . ((Frege u) . x),x) . y = f . y by FINSEQOP:def 1; :: thesis: verum

end;

hence [:b:] . ((Frege u) . x),x = the_unity_wrt [:b:] by A5, A6, FUNCT_1:9; :: thesis: verum