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

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:18;
for v being set 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:9; :: thesis: verum

end;

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