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
A5: 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
A6: 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

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 A5;
hence (P . x,f) . i = (Q . x,f) . i by A6; :: thesis: verum

end;

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