let P, Q 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 (P . (x,d)) . i = (p . i) . (x,(d . i)) ) & ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (Q . (x,d)) . i = (p . i) . (x,(d . i)) ) implies P = Q )
assume that
A4:
for x being Element of X
for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (p . i) . (x,(f . i))
and
A5:
for x being Element of X
for f being Element of product F
for i being Element of dom F holds (Q . (x,f)) . i = (p . i) . (x,(f . i))
; P = Q
now for x being Element of X
for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . ilet x be
Element of
X;
for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . ilet f be
Element of
product F;
for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . ilet i be
Element of
dom F;
(P . (x,f)) . i = (Q . (x,f)) . i
(P . (x,f)) . i = (p . i) . (
x,
(f . i))
by A4;
hence
(P . (x,f)) . i = (Q . (x,f)) . i
by A5;
verum end;
hence
P = Q
by Th5; verum