let x, y be Function of (([|A,B|] #) . pj),([|A,B|] . rj); ( ( 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))]
; x = y
let h be Element of ([|A,B|] #) . pj; FUNCT_2:def 8 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; verum