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 (Class E)),(Class (n -placesOf E)) st b_{1} = n -tuple2Class E holds

b_{1} is Function-like

b

hence
for b_{1} being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b_{1} = n -tuple2Class E holds

b_{1} is Function-like
by Lm11; :: thesis: verum

end;b

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

b_{1} is Function-like

b

then reconsider m = n as zero Nat ;

set En = n -placesOf E;

reconsider f1 = E -class as Function of U,(Class E) ;

reconsider r1 = E -class as Relation of U,(Class E) ;

reconsider r2 = r1 ~ as Relation of (Class E),U ;

reconsider f3 = m -placesOf r2 as PartFunc of (m -tuples_on (Class E)),(m -tuples_on U) ;

reconsider f4 = (n -placesOf E) -class as Function of (n -tuples_on U),(Class (n -placesOf E)) ;

f3 * f4 is Function-like ;

hence for b_{1} being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b_{1} = n -tuple2Class E holds

b_{1} is Function-like
; :: thesis: verum

end;set En = n -placesOf E;

reconsider f1 = E -class as Function of U,(Class E) ;

reconsider r1 = E -class as Relation of U,(Class E) ;

reconsider r2 = r1 ~ as Relation of (Class E),U ;

reconsider f3 = m -placesOf r2 as PartFunc of (m -tuples_on (Class E)),(m -tuples_on U) ;

reconsider f4 = (n -placesOf E) -class as Function of (n -tuples_on U),(Class (n -placesOf E)) ;

f3 * f4 is Function-like ;

hence for b

b