set RR = n -placesOf R;

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

end;

suppose
not n is zero
; :: thesis: for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total

b

then reconsider nn = n as non zero Nat ;

nn -placesOf R is total ;

hence for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total
; :: thesis: verum

end;nn -placesOf R is total ;

hence for b

b

suppose
n is zero
; :: thesis: for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total

b

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_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total
by PARTFUN1:def 2; :: thesis: verum

end;nn -placesOf R = {[{},{}]} by Lm4;

then dom (n -placesOf R) = {{}} by RELAT_1:9

.= nn -tuples_on X by FOMODEL0:10 ;

hence for b

b