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

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

A3: now

let y be set ; :: 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, Def10;
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 A2, A3, FUNCT_1:2; :: thesis: [:b:] . (x,f) = x

A4: now

let y be set ; :: 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, Def10;
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 A2, A4, FUNCT_1:2; :: thesis: verum

end;

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