set RR = n -placesOf R;
per cases ( not n is zero or n is zero ) ;
suppose not n is zero ; :: thesis: for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is total
then reconsider nn = n as non zero Nat ;
nn -placesOf R is total ;
hence for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is total ; :: thesis: verum
end;
suppose n is zero ; :: thesis: for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 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 b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is total by PARTFUN1:def 2; :: thesis: verum
end;
end;