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

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

hence
P = Q
by Th5; :: thesis: verumfor 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;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