let P, Q 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 (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)) ; :: thesis: P = Q

now :: thesis: 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)) . i

let x be Element of X; :: thesis: for f being Element of product F
for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i
let f be Element of product F; :: thesis: for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i
let i be Element of dom F; :: thesis: (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; :: thesis: verum

end;

hence P = Q by Th5; :: thesis: verum