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

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 )

hence
f is_a_unity_wrt [:b:]
by BINOP_1:3; :: thesis: verum( [:b:] . (f,x) = x & [:b:] . (x,f) = x )

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

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

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

end;A3: now :: thesis: for y being object st y in dom a holds

([:b:] . (f,x)) . y = x . y

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

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

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

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