let X, Y be set ; :: thesis: for f being Function of X,Y
for V being ManySortedSet of Y
for E being one-to-one ManySortedSet of X holds (V * f) * (E ") is Function of (rng E),(rng V)
let f be Function of X,Y; :: thesis: for V being ManySortedSet of Y
for E being one-to-one ManySortedSet of X holds (V * f) * (E ") is Function of (rng E),(rng V)
let V be ManySortedSet of Y; :: thesis: for E being one-to-one ManySortedSet of X holds (V * f) * (E ") is Function of (rng E),(rng V)
let E be one-to-one ManySortedSet of X; :: thesis: (V * f) * (E ") is Function of (rng E),(rng V)

per cases ( Y <> {} or Y = {} ) ;

suppose A1: Y <> {} ; :: thesis: (V * f) * (E ") is Function of (rng E),(rng V)

rng f c= Y ;
then A2: rng f c= dom V by PARTFUN1:def 2;
rng (E ") = dom E by FUNCT_1:33
.= X by PARTFUN1:def 2
.= dom f by A1, PARTFUN1:def 2
.= dom (V * f) by A2, RELAT_1:27 ;
then A3: dom ((V * f) * (E ")) = dom (E ") by RELAT_1:27
.= rng E by FUNCT_1:33 ;
A4: rng ((V * f) * (E ")) c= rng (V * f) by RELAT_1:26;
rng (V * f) c= rng V by RELAT_1:26;
hence (V * f) * (E ") is Function of (rng E),(rng V) by A3, A4, XBOOLE_1:1, FUNCT_2:2; :: thesis: verum

end;

suppose Y = {} ; :: thesis: (V * f) * (E ") is Function of (rng E),(rng V)

then A5: ( V * f = {} & rng V = {} ) ;
then A6: (V * f) * (E ") = {} ;
then ( dom ((V * f) * (E ")) = {} & rng ((V * f) * (E ")) = {} ) ;
then ( dom ((V * f) * (E ")) c= rng E & rng ((V * f) * (E ")) c= rng V ) by XBOOLE_1:2;
then reconsider g = (V * f) * (E ") as PartFunc of (rng E),(rng V) by RELSET_1:4;
g is quasi_total by A5, A6, FUNCT_2:def 1;
hence (V * f) * (E ") is Function of (rng E),(rng V) ; :: thesis: verum

end;

end;