let a be Domain-Sequence; :: thesis: for d, d9 being BinOp of (product a) st ( for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) holds

d = d9

let d, d9 be BinOp of (product a); :: thesis: ( ( for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) implies d = d9 )

assume A1: for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ; :: thesis: d = d9

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) holds

d = d9

let d, d9 be BinOp of (product a); :: thesis: ( ( for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) implies d = d9 )

assume A1: for f, g being Element of product a

for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ; :: thesis: d = d9

now :: thesis: for f, g being Element of product a holds d . (f,g) = d9 . (f,g)

hence
d = d9
; :: thesis: verumlet f, g be Element of product a; :: thesis: d . (f,g) = d9 . (f,g)

( dom (d . (f,g)) = dom a & dom (d9 . (f,g)) = dom a ) by CARD_3:9;

hence d . (f,g) = d9 . (f,g) by A1; :: thesis: verum

end;( dom (d . (f,g)) = dom a & dom (d9 . (f,g)) = dom a ) by CARD_3:9;

hence d . (f,g) = d9 . (f,g) by A1; :: thesis: verum