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:18;

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:11; :: thesis: verum

end;

dom ([:b:] . f,x) = dom a by CARD_3:18;
hence [:b:] . f,x = x by A2, A3, FUNCT_1:9; :: 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:11; :: thesis: verum

end;

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

end;

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