let X be set ; :: thesis: for f being homogeneous PartFunc of (X * ),X holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )
let f be homogeneous PartFunc of (X * ),X; :: thesis: ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )

then rng f = {} ;
then f = {} ;
hence ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X ) by Th8, Th21; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )

hence ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X ) by Lm1; :: thesis: verum

end;

end;