let x, y be Function of (([|A,B|] #) . pj),([|A,B|] . rj); :: thesis: ( ( for h being Function st h in ([|A,B|] #) . pj holds
x . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds
y . h = [(f . (pr1 h)),(g . (pr2 h))] ) implies x = y )
assume that
A26: for h being Function st h in ([|A,B|] #) . pj holds
x . h = [(f . (pr1 h)),(g . (pr2 h))] and
A27: for h being Function st h in ([|A,B|] #) . pj holds
y . h = [(f . (pr1 h)),(g . (pr2 h))] ; :: thesis: x = y
let h be Element of ([|A,B|] #) . pj; :: according to FUNCT_2:def 8 :: thesis: x . h = y . h
h in ([|A,B|] #) . pj ;
then h in product ([|A,B|] * pj) by FINSEQ_2:def 5;
then consider h1 being Function such that
A28: h1 = h and
dom h1 = dom ([|A,B|] * pj) and
for z being object st z in dom ([|A,B|] * pj) holds
h1 . z in ([|A,B|] * pj) . z by CARD_3:def 5;
x . h1 = [(f . (pr1 h1)),(g . (pr2 h1))] by A26, A28;
hence x . h = y . h by A27, A28; :: thesis: verum