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 A1: ( f is one-to-one & g = f " ) ; :: thesis: ( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
then A2: ( rng f = dom g & rng g = dom f ) by FUNCT_1:55;
A3: ( the carrier of (Image (f | R)) c= the carrier of T & the carrier of R c= the carrier of S ) by YELLOW_0:def 13;
A4: ( dom g = the carrier of T & dom f = the carrier of S ) by FUNCT_2:def 1;
set h = g | (Image (f | R));
A5: dom (g | (Image (f | R))) = the carrier of (Image (f | R)) by FUNCT_2:def 1;
rng (g | (Image (f | R))) c= the carrier of R

proof

let y be set ; :: 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 set such that
A6: ( x in dom (g | (Image (f | R))) & y = (g | (Image (f | R))) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of (Image (f | R)) by A6;
consider a being Element of R such that
A7: (f | R) . a = x by YELLOW_2:12;
( y = g . x & x in rng f & a in the carrier of R ) by A2, A3, A4, A5, A6, Th7;
then ( f . y = x & f . a = x & y in dom f & a in dom f ) by A1, A3, A4, A7, Th7, FUNCT_1:54;
then y = a by A1, FUNCT_1:def 8;
hence y in the carrier of R ; :: thesis: verum

end;

hence g | (Image (f | R)) is Function of (Image (f | R)),R by A5, RELSET_1:11; :: thesis: g | (Image (f | R)) = (f | R) "
A8: f | R is one-to-one by A1, Th8;
then A9: ( dom ((f | R) " ) = rng (f | R) & rng ((f | R) " ) = dom (f | R) ) by FUNCT_1:55;
A10: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def 15;

now

let x be set ; :: thesis: ( x in the carrier of (Image (f | R)) implies (g | (Image (f | R))) . x = ((f | R) " ) . x )
assume A11: x in the carrier of (Image (f | R)) ; :: thesis: (g | (Image (f | R))) . x = ((f | R) " ) . x
then consider y being set such that
A12: ( y in dom (f | R) & x = (f | R) . y ) by A10, FUNCT_1:def 5;
dom (f | R) = the carrier of R by FUNCT_2:def 1;
then ( x = f . y & y in the carrier of S ) by A3, A12, Th7;
then ( y = g . x & y = ((f | R) " ) . x ) by A1, A4, A8, A12, FUNCT_1:54;
hence (g | (Image (f | R))) . x = ((f | R) " ) . x by A11, Th7; :: thesis: verum

end;

hence g | (Image (f | R)) = (f | R) " by A5, A9, A10, FUNCT_1:9; :: thesis: verum