let X be non empty set ; 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; 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); ( ( 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
; f = g
now 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;
for d being Element of product F holds f . (x,d) = g . (x,d)let d be
Element of
product F;
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;
verum end;
hence
f = g
by BINOP_1:2; verum