let f, g be non-empty Function; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: (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 ;
:: thesis: verum