let x, y be set ; for g being Function
for A being set st not y in g .: (A \ {x}) holds
(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
let g be Function; for A being set st not y in g .: (A \ {x}) holds
(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
let A be set ; ( not y in g .: (A \ {x}) implies (g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y} )
assume A1:
not y in g .: (A \ {x})
; (g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}
thus
(g +* (x .--> y)) .: (A \ {x}) c= ((g +* (x .--> y)) .: A) \ {y}
XBOOLE_0:def 10 ((g +* (x .--> y)) .: A) \ {y} c= (g +* (x .--> y)) .: (A \ {x})proof
let u be
object ;
TARSKI:def 3 ( not u in (g +* (x .--> y)) .: (A \ {x}) or u in ((g +* (x .--> y)) .: A) \ {y} )
A2:
dom (x .--> y) = {x}
;
assume A3:
u in (g +* (x .--> y)) .: (A \ {x})
;
u in ((g +* (x .--> y)) .: A) \ {y}
then consider z being
object such that A4:
z in dom (g +* (x .--> y))
and A5:
z in A \ {x}
and A6:
u = (g +* (x .--> y)) . z
by FUNCT_1:def 6;
A7:
not
z in {x}
by A5, XBOOLE_0:def 5;
then A8:
z in dom g
by A4, A2, FUNCT_4:12;
u = g . z
by A6, A7, A2, FUNCT_4:11;
then
u <> y
by A1, A5, A8, FUNCT_1:def 6;
then A9:
not
u in {y}
by TARSKI:def 1;
(g +* (x .--> y)) .: (A \ {x}) c= (g +* (x .--> y)) .: A
by RELAT_1:123;
hence
u in ((g +* (x .--> y)) .: A) \ {y}
by A3, A9, XBOOLE_0:def 5;
verum
end;
let u be object ; TARSKI:def 3 ( not u in ((g +* (x .--> y)) .: A) \ {y} or u in (g +* (x .--> y)) .: (A \ {x}) )
assume A10:
u in ((g +* (x .--> y)) .: A) \ {y}
; u in (g +* (x .--> y)) .: (A \ {x})
then consider z being object such that
A11:
z in dom (g +* (x .--> y))
and
A12:
z in A
and
A13:
u = (g +* (x .--> y)) . z
by FUNCT_1:def 6;
then
z in A \ {x}
by A12, XBOOLE_0:def 5;
hence
u in (g +* (x .--> y)) .: (A \ {x})
by A11, A13, FUNCT_1:def 6; verum