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

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)

hence
f = g
by BINOP_1:2; :: thesis: verumfor 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;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