let f, g be non-empty Function; :: thesis: for i being object
for A being set st A c= () /\ (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 +* g)) holds
(proj (f,i)) .: A = (proj ((f +* g),i)) .: A

let A be set ; :: thesis: ( A c= () /\ (product (f +* g)) implies (proj (f,i)) .: A = (proj ((f +* g),i)) .: A )
assume A1: A c= () /\ (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 ;
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 ; :: 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 ;
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 ; :: thesis: verum
end;
hence (proj (f,i)) .: A = (proj ((f +* g),i)) .: A by TARSKI:2; :: thesis: verum