let X be non empty set ; :: thesis: for F being Domain-Sequence
for f, g being Function of [:X,():],() 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,():],() 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,():],(); :: 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 ; :: thesis: verum
end;
hence f = g by BINOP_1:2; :: thesis: verum