let a be Domain-Sequence; :: thesis: for d, d' being UnOp of product a st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d' . f) . i ) holds
d = d'
let d, d' be UnOp of product a; :: thesis: ( ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d' . f) . i ) implies d = d' )
assume A1: for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d' . f) . i ; :: thesis: d = d'

now

let f be Element of product a; :: thesis: d . f = d' . f
A2: ( dom (d . f) = dom a & dom (d' . f) = dom a ) by CARD_3:18;
for x being set st x in dom a holds
(d . f) . x = (d' . f) . x by A1;
hence d . f = d' . f by A2, FUNCT_1:9; :: thesis: verum

end;

hence d = d' by FUNCT_2:113; :: thesis: verum