let X be non empty set ; :: thesis: for F being Domain-Sequence
for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds
f = g
let F be Domain-Sequence; :: thesis: for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds
f = g
let f, g be Function of [:X,(product F):],(product F); :: thesis: ( ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) implies f = g )
assume A1: for x being Element of X
for d being Element of product F
for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ; :: thesis: f = g

now :: thesis: for x being Element of X
for d being Element of product F holds f . (x,d) = g . (x,d)

let x be Element of X; :: thesis: for d being Element of product F holds f . (x,d) = g . (x,d)
let d be Element of product F; :: thesis: f . (x,d) = g . (x,d)
A2: ( dom (f . (x,d)) = dom F & dom (g . (x,d)) = dom F ) by CARD_3:9;
for v being object st v in dom F holds
(f . (x,d)) . v = (g . (x,d)) . v by A1;
hence f . (x,d) = g . (x,d) by A2, FUNCT_1:2; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum