let p, q be Function of (product F),(product G); :: thesis: ( ( for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (p . x) . i = hi . (x . i) ) ) & ( for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (q . x) . i = hi . (x . i) ) ) implies p = q )
assume that
A8: for f being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (p . f) . i = hi . (f . i) ) and
A9: for f being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (q . f) . i = hi . (f . i) ) ; :: thesis: p = q
now :: thesis: for f being Element of product F holds p . f = q . f
let f be Element of product F; :: thesis: p . f = q . f
A10: ( dom (p . f) = dom G & dom (q . f) = dom G ) by CARD_3:9;
now :: thesis: for i being object st i in dom (p . f) holds
(p . f) . i = (q . f) . i
let i be object ; :: thesis: ( i in dom (p . f) implies (p . f) . i = (q . f) . i )
assume i in dom (p . f) ; :: thesis: (p . f) . i = (q . f) . i
then A12: i in dom h by A1, CARD_3:9;
A13: ex hi being Function of (F . i),(G . i) st
( hi = h . i & (p . f) . i = hi . (f . i) ) by A8, A12;
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (q . f) . i = hi . (f . i) ) by A9, A12;
hence (p . f) . i = (q . f) . i by A13; :: thesis: verum
end;
hence p . f = q . f by A10, FUNCT_1:2; :: thesis: verum
end;
hence p = q by FUNCT_2:def 8; :: thesis: verum