let f be non-empty Function; 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 ; 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 ; ( 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 )
; (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;