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 V7() & 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 V7() & 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 V7() & 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 V7() & 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 V7() 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

A11: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def 15;

A12: f | R is V7() by A1, Th7;

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

for f being Function of S,T

for g being Function of T,S st f is V7() & 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 V7() & 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 V7() & 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 V7() & 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 V7() 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

hence
g | (Image (f | R)) is Function of (Image (f | R)),R
by A4, RELSET_1:4; :: thesis: g | (Image (f | R)) = (f | R) "
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;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

A11: rng (f | R) = the carrier of (Image (f | R)) by YELLOW_0:def 15;

A12: f | R is V7() 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

dom ((f | R) ") = rng (f | R)
by A12, FUNCT_1:33;(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;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

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