let X, Y, Z be set ; :: thesis: for f being quasi_total Relation of X,Y
for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total
let f be quasi_total Relation of X,Y; :: thesis: for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total
let g be quasi_total Relation of Y,Z; :: thesis: ( ( not Y = {} or Z = {} or X = {} ) implies f * g is quasi_total )
assume A1: ( not Y = {} or Z = {} or X = {} ) ; :: thesis: f * g is quasi_total

per cases ( Z <> {} or Z = {} ) ;
:: according to FUNCT_2:def 1

case A2: Z <> {} ; :: thesis: X = dom (f * g)

then A3: dom g = Y by Def1;
( dom f = X & rng f c= Y ) by A1, A2, Def1;
hence X = dom (f * g) by A3, RELAT_1:27; :: thesis: verum

end;

case Z = {} ; :: thesis: f * g = {}

hence f * g = {} ; :: thesis: verum

end;

end;