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_{1}[ 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_{1}[x,y]

A3: ( dom f = dom a & ( for x being object st x in dom a holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A2);

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:] )

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

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

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

( $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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in dom a implies ex y being object st S_{1}[x,y] )

assume x in dom a ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider i = x as Element of dom a ;

take the_unity_wrt (b . i) ; :: thesis: S_{1}[x, the_unity_wrt (b . i)]

thus S_{1}[x, the_unity_wrt (b . i)]
; :: thesis: verum

end;assume x in dom a ; :: thesis: ex y being object st S

then reconsider i = x as Element of dom a ;

take the_unity_wrt (b . i) ; :: thesis: S

thus S

A3: ( dom f = dom a & ( for x being object st x in dom a holds

S

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

f . x in a . x

then reconsider f = f as Element of product a by A3, CARD_3:9;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;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

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

([: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;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

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

then
f is_a_unity_wrt [:b:]
by Th19;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;( 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

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

dom ([:b:] . (x,((Frege u) . x))) = dom a
by CARD_3:9;([: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;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

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