let S, T be non empty RelStr ; :: thesis: for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is one-to-one & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let R be non empty SubRelStr of S; :: thesis: for f being Function of S,T
for g being Function of T,S st f is one-to-one & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let f be Function of S,T; :: thesis: for g being Function of T,S st f is one-to-one & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
let g be Function of T,S; :: thesis: ( f is one-to-one & g = f " implies ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " ) )
assume that
A1: f is one-to-one and
A2: g = f " ; :: thesis: ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
set h = g | (Image (f | R));
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: dom (g | (Image (f | R))) = the carrier of (Image (f | R)) by FUNCT_2:def 1;
A5: the carrier of R c= the carrier of S by YELLOW_0:def 13;
rng (g | (Image (f | R))) c= the carrier of R

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (g | (Image (f | R))) or y in the carrier of R )
assume y in rng (g | (Image (f | R))) ; :: thesis: y in the carrier of R
then consider x being object such that
A6: x in dom (g | (Image (f | R))) and
A7: y = (g | (Image (f | R))) . x by FUNCT_1:def 3;
reconsider x = x as Element of (Image (f | R)) by A6;
consider a being Element of R such that
A8: (f | R) . a = x by YELLOW_2:10;
A9: f . a = x by A8, Th6;
A10: a in the carrier of R ;
y = g . x by A7, Th6;
hence y in the carrier of R by A1, A2, A5, A3, A10, A9, FUNCT_1:32; :: thesis: verum

end;

hence g | (Image (f | R)) is Function of (Image (f | R)),R by A4, RELSET_1:4; :: thesis: g | (Image (f | R)) = (f | R) "
A11: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def 15;
A12: f | R is one-to-one by A1, Th7;

A13: now :: thesis: for x being object st x in the carrier of (Image (f | R)) holds
(g | (Image (f | R))) . x = ((f | R) ") . x

let x be object ; :: thesis: ( x in the carrier of (Image (f | R)) implies (g | (Image (f | R))) . x = ((f | R) ") . x )
A14: dom (f | R) = the carrier of R by FUNCT_2:def 1;
assume A15: x in the carrier of (Image (f | R)) ; :: thesis: (g | (Image (f | R))) . x = ((f | R) ") . x
then consider y being object such that
A16: y in dom (f | R) and
A17: x = (f | R) . y by A11, FUNCT_1:def 3;
A18: y = ((f | R) ") . x by A12, A16, A17, FUNCT_1:32;
x = f . y by A16, A17, Th6;
then y = g . x by A1, A2, A5, A3, A16, A14, FUNCT_1:32;
hence (g | (Image (f | R))) . x = ((f | R) ") . x by A15, A18, Th6; :: thesis: verum

end;

dom ((f | R) ") = rng (f | R) by A12, FUNCT_1:33;
hence g | (Image (f | R)) = (f | R) " by A4, A11, A13, FUNCT_1:2; :: thesis: verum