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;