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 = (b . i) . ((f . i),(g . i)) ) & ( for f, g being Element of product a

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

assume that

A5: for f, g being Element of product a

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

A6: for f, g being Element of product a

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

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

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

assume that

A5: for f, g being Element of product a

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

A6: for f, g being Element of product a

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

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

hence
d = d9
by Th16; :: thesis: verumfor i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i

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

let i be Element of dom a; :: thesis: (d . (f,g)) . i = (d9 . (f,g)) . i

thus (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A5

.= (d9 . (f,g)) . i by A6 ; :: thesis: verum

end;let i be Element of dom a; :: thesis: (d . (f,g)) . i = (d9 . (f,g)) . i

thus (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A5

.= (d9 . (f,g)) . i by A6 ; :: thesis: verum