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;

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 )
;

end;

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

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;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

A8:
i in {i}
by TARSKI:def 1;
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;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

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