let X, Y be set ; for f being Function of X,Y st Y <> {} holds
( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
let f be Function of X,Y; ( Y <> {} implies ( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ) )
assume A1:
Y <> {}
; ( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
thus
( rng f = Y implies for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )
( ( for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h ) implies rng f = Y )proof
assume A2:
rng f = Y
;
for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h
let Z be
set ;
( Z <> {} implies for g, h being Function of Y,Z st g * f = h * f holds
g = h )
assume A3:
Z <> {}
;
for g, h being Function of Y,Z st g * f = h * f holds
g = h
let g,
h be
Function of
Y,
Z;
( g * f = h * f implies g = h )
(
dom g = Y &
dom h = Y )
by A3, Def1;
hence
(
g * f = h * f implies
g = h )
by A2, FUNCT_1:86;
verum
end;
assume A4:
for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h
; rng f = Y
for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h
proof
let g,
h be
Function;
( dom g = Y & dom h = Y & g * f = h * f implies g = h )
assume that A5:
dom g = Y
and A6:
dom h = Y
;
( not g * f = h * f or g = h )
A7:
rng g <> {}
by A1, A5, RELAT_1:42;
A8:
g is
Function of
Y,
((rng g) \/ (rng h))
by A5, Th2, XBOOLE_1:7;
h is
Function of
Y,
((rng g) \/ (rng h))
by A6, Th2, XBOOLE_1:7;
hence
( not
g * f = h * f or
g = h )
by A4, A7, A8;
verum
end;
hence
rng f = Y
by FUNCT_1:16; verum