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

(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