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:
defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in dom a implies ex y being object st S1[x,y] )
assume x in dom a ; :: thesis: ex y being object st S1[x,y]
then reconsider i = x as Element of dom a ;
take the_unity_wrt (b . i) ; :: thesis: S1[x, the_unity_wrt (b . i)]
thus S1[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
S1[x,f . x] ) ) from
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 ;
let x be Element of product a; :: according to FINSEQOP:def 1 :: thesis: ( [:b:] . (x,(() . x)) = the_unity_wrt [:b:] & [:b:] . ((() . x),x) = the_unity_wrt [:b:] )
A5: now :: thesis: for y being object st y in dom a holds
([:b:] . (x,(() . x))) . y = f . y
let y be object ; :: thesis: ( y in dom a implies ([:b:] . (x,(() . x))) . y = f . y )
assume y in dom a ; :: thesis: ([:b:] . (x,(() . 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 ;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (x,(() . x))) . i = (b . i) . ((x . i),((() . x) . i)) ) by ;
hence ([:b:] . (x,(() . 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:] . ((() . x),x)) . y = f . y
let y be object ; :: thesis: ( y in dom a implies ([:b:] . ((() . x),x)) . y = f . y )
assume y in dom a ; :: thesis: ([:b:] . ((() . 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 ;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . ((() . x),x)) . i = (b . i) . (((() . x) . i),(x . i)) ) by ;
hence ([:b:] . ((() . x),x)) . y = f . y by A9; :: thesis: verum
end;
dom ([:b:] . (x,(() . x))) = dom a by CARD_3:9;
hence [:b:] . (x,(() . x)) = the_unity_wrt [:b:] by ; :: thesis: [:b:] . ((() . x),x) = the_unity_wrt [:b:]
dom ([:b:] . ((() . x),x)) = dom a by CARD_3:9;
hence [:b:] . ((() . x),x) = the_unity_wrt [:b:] by ; :: thesis: verum