let a be Domain-Sequence; :: thesis: for b being BinOps of a
for f being Element of product a st ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) holds
f is_a_unity_wrt [:b:]
let b be BinOps of a; :: thesis: for f being Element of product a st ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) holds
f is_a_unity_wrt [:b:]
let f be Element of product a; :: thesis: ( ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) implies f is_a_unity_wrt [:b:] )
assume A1: for i being Element of dom a holds f . i is_a_unity_wrt b . i ; :: thesis: f is_a_unity_wrt [:b:]

now :: thesis: for x being Element of product a holds
( [:b:] . (f,x) = x & [:b:] . (x,f) = x )

let x be Element of product a; :: thesis: ( [:b:] . (f,x) = x & [:b:] . (x,f) = x )

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

let y be object ; :: thesis: ( y in dom a implies ([:b:] . (f,x)) . y = x . y )
assume y in dom a ; :: thesis: ([:b:] . (f,x)) . y = x . y
then reconsider i = y as Element of dom a ;
( ([:b:] . (f,x)) . i = (b . i) . ((f . i),(x . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence ([:b:] . (f,x)) . y = x . y by BINOP_1:3; :: thesis: verum

end;

dom ([:b:] . (f,x)) = dom a by CARD_3:9;
hence [:b:] . (f,x) = x by A3, CARD_3:9; :: thesis: [:b:] . (x,f) = x

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

let y be object ; :: thesis: ( y in dom a implies ([:b:] . (x,f)) . y = x . y )
assume y in dom a ; :: thesis: ([:b:] . (x,f)) . y = x . y
then reconsider i = y as Element of dom a ;
( ([:b:] . (x,f)) . i = (b . i) . ((x . i),(f . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence ([:b:] . (x,f)) . y = x . y by BINOP_1:3; :: thesis: verum

end;

dom ([:b:] . (x,f)) = dom a by CARD_3:9;
hence [:b:] . (x,f) = x by A4, CARD_3:9; :: thesis: verum

end;

hence f is_a_unity_wrt [:b:] by BINOP_1:3; :: thesis: verum