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 set such that
A3: a in dom (f | X) and
A4: (f | X) . a = x by A2, FUNCT_1:def 5;
dom (f | X) = (dom f) /\ X by RELAT_1:90;
then A5: a in X by A3, XBOOLE_0:def 4;
dom ((f | X) " ) = rng (f | X) by A1, FUNCT_1:54;
hence (f * ((f | X) " )) . x = f . (((f | X) " ) . x) by A2, FUNCT_1:23
.= f . a by A1, A3, A4, FUNCT_1:54
.= x by A4, A5, FUNCT_1:72 ;
:: thesis: verum