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 f = {} ;
hence ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X ) by Th5, Th17; :: 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;