let S, T be non empty RelStr ; 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; 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; 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; ( 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 "
; ( 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
hence
g | (Image (f | R)) is Function of (Image (f | R)),R
by A4, RELSET_1:4; 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 V7()
by A1, Th7;
A13:
now for x being object st x in the carrier of (Image (f | R)) holds
(g | (Image (f | R))) . x = ((f | R) ") . xlet x be
object ;
( 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))
;
(g | (Image (f | R))) . x = ((f | R) ") . xthen 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;
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; verum