set RR = n -placesOf R;

per cases ( not n is zero or n is zero ) ;

suppose not n is zero ; :: thesis: for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is total

then reconsider nn = n as non zero Nat ;
nn -placesOf R is total ;
hence for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is total ; :: thesis: verum

end;

suppose n is zero ; :: thesis: for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is total

then reconsider nn = n as zero Nat ;
nn -placesOf R = {[{},{}]} by Lm4;
then dom (n -placesOf R) = {{}} by RELAT_1:9
.= nn -tuples_on X by FOMODEL0:10 ;
hence for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum

end;

end;