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 ;
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 ;
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 ; :: 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 ; :: 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 ;
then {} in rng (f +* (i,X)) by ;
then product (f +* (i,X)) = {} by CARD_3:26;
hence (proj (f,i)) .: (product (f +* (i,X))) = X by A9; :: thesis: verum
end;
end;