let f be Function; :: thesis: for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) ")) . x = x
let X, x be set ; :: thesis: ( f | X is one-to-one & x in rng (f | X) implies (f * ((f | X) ")) . x = x )
set g = f | X;
assume that
A1: f | X is one-to-one and
A2: x in rng (f | X) ; :: thesis: (f * ((f | X) ")) . x = x
consider a being object such that
A3: a in dom (f | X) and
A4: (f | X) . a = x by A2, FUNCT_1:def 3;
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A5: a in X by A3, XBOOLE_0:def 4;
dom ((f | X) ") = rng (f | X) by A1, FUNCT_1:32;
hence (f * ((f | X) ")) . x = f . (((f | X) ") . x) by A2, FUNCT_1:13
.= f . a by A1, A3, A4, FUNCT_1:32
.= x by A4, A5, FUNCT_1:49 ;
:: thesis: verum