let a be Domain-Sequence; :: thesis: for d, d9 being UnOp of (product a) st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds
d = d9
let d, d9 be UnOp of (product a); :: thesis: ( ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) implies d = d9 )
assume A1: for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ; :: thesis: d = d9
now :: thesis: for f being Element of product a holds d . f = d9 . f
let f be Element of product a; :: thesis: d . f = d9 . f
( dom (d . f) = dom a & dom (d9 . f) = dom a ) by CARD_3:9;
hence d . f = d9 . f by A1; :: thesis: verum
end;
hence d = d9 by FUNCT_2:63; :: thesis: verum