let f, g be non-empty Function; :: thesis: for i being object
for A being set st A c= (product f) /\ (product (f +* g)) holds
(proj (f,i)) .: A = (proj ((f +* g),i)) .: A
let i be object ; :: thesis: for A being set st A c= (product f) /\ (product (f +* g)) holds
(proj (f,i)) .: A = (proj ((f +* g),i)) .: A
let A be set ; :: thesis: ( A c= (product f) /\ (product (f +* g)) implies (proj (f,i)) .: A = (proj ((f +* g),i)) .: A )
assume A1: A c= (product f) /\ (product (f +* g)) ; :: thesis: (proj (f,i)) .: A = (proj ((f +* g),i)) .: A
for y being object holds
( y in (proj (f,i)) .: A iff y in (proj ((f +* g),i)) .: A )

proof

let y be object ; :: thesis: ( y in (proj (f,i)) .: A iff y in (proj ((f +* g),i)) .: A )

hereby :: thesis: ( y in (proj ((f +* g),i)) .: A implies y in (proj (f,i)) .: A )

assume y in (proj (f,i)) .: A ; :: thesis: y in (proj ((f +* g),i)) .: A
then consider x being object such that
A2: ( x in dom (proj (f,i)) & x in A & y = (proj (f,i)) . x ) by FUNCT_1:def 6;
x in product (f +* g) by A1, A2, XBOOLE_0:def 4;
then A4: x in dom (proj ((f +* g),i)) by CARD_3:def 16;
y = (proj ((f +* g),i)) . x by A2, A1, Th21;
hence y in (proj ((f +* g),i)) .: A by A2, A4, FUNCT_1:def 6; :: thesis: verum

end;

assume y in (proj ((f +* g),i)) .: A ; :: thesis: y in (proj (f,i)) .: A
then consider x being object such that
A5: ( x in dom (proj ((f +* g),i)) & x in A & y = (proj ((f +* g),i)) . x ) by FUNCT_1:def 6;
x in product f by A1, A5, XBOOLE_0:def 4;
then A7: x in dom (proj (f,i)) by CARD_3:def 16;
y = (proj (f,i)) . x by A5, A1, Th21;
hence y in (proj (f,i)) .: A by A5, A7, FUNCT_1:def 6; :: thesis: verum

end;

hence (proj (f,i)) .: A = (proj ((f +* g),i)) .: A by TARSKI:2; :: thesis: verum