let f, g be non-empty Function; for i, x being object st x in (product f) /\ (product (f +* g)) holds
(proj (f,i)) . x = (proj ((f +* g),i)) . x
let i, x be object ; ( x in (product f) /\ (product (f +* g)) implies (proj (f,i)) . x = (proj ((f +* g),i)) . x )
assume A1:
x in (product f) /\ (product (f +* g))
; (proj (f,i)) . x = (proj ((f +* g),i)) . x
then
x in product f
by XBOOLE_0:def 4;
then reconsider h = x as Function ;
( x in product f & x in product (f +* g) )
by A1, XBOOLE_0:def 4;
then A2:
( x in dom (proj (f,i)) & x in dom (proj ((f +* g),i)) )
by CARD_3:def 16;
hence (proj (f,i)) . x =
h . i
by CARD_3:def 16
.=
(proj ((f +* g),i)) . x
by A2, CARD_3:def 16
;
verum