let f be non-empty Function; :: thesis: for X being set
for i being object st i in dom f & X c= f . i holds
(proj (f,i)) .: (product (f +* (i,X))) = X
let X be set ; :: thesis: for i being object st i in dom f & X c= f . i holds
(proj (f,i)) .: (product (f +* (i,X))) = X
let i be object ; :: thesis: ( i in dom f & X c= f . i implies (proj (f,i)) .: (product (f +* (i,X))) = X )
assume A1: ( i in dom f & X c= f . i ) ; :: thesis: (proj (f,i)) .: (product (f +* (i,X))) = X
then A2: f +* (i,X) = f +* (i .--> X) by FUNCT_7:def 3
.= f +* ({i} --> X) by FUNCOP_1:def 9 ;
A3: i in dom (f +* (i,X)) by A1, FUNCT_7:30;

per cases ( not X is empty or X is empty ) ;

suppose A4: not X is empty ; :: thesis: (proj (f,i)) .: (product (f +* (i,X))) = X

{i} c= dom f by A1, ZFMISC_1:31;
then A5: dom ({i} --> X) c= dom f ;
A6: for j being object st j in dom ({i} --> X) holds
({i} --> X) . j c= f . j

proof

let j be object ; :: thesis: ( j in dom ({i} --> X) implies ({i} --> X) . j c= f . j )
assume A7: j in dom ({i} --> X) ; :: thesis: ({i} --> X) . j c= f . j
then i = j by TARSKI:def 1;
hence ({i} --> X) . j c= f . j by A1, A7, FUNCOP_1:7; :: thesis: verum

end;

A8: i in {i} by TARSKI:def 1;
then i in dom ({i} --> X) ;
then (proj (f,i)) .: (product (f +* ({i} --> X))) = ({i} --> X) . i by A5, A6, A4, Th25;
hence (proj (f,i)) .: (product (f +* (i,X))) = X by A2, A8, FUNCOP_1:7; :: thesis: verum

end;

suppose A9: X is empty ; :: thesis: (proj (f,i)) .: (product (f +* (i,X))) = X

then (f +* (i,X)) . i is empty by A1, FUNCT_7:31;
then {} in rng (f +* (i,X)) by A3, FUNCT_1:3;
then product (f +* (i,X)) = {} by CARD_3:26;
hence (proj (f,i)) .: (product (f +* (i,X))) = X by A9; :: thesis: verum

end;

end;