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

suppose not n is zero ; :: thesis: for b₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ is Function-like

hence for b₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ is Function-like by Lm11; :: thesis: verum

end;

suppose n is zero ; :: thesis: for b₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ is Function-like

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₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ is Function-like ; :: thesis: verum

end;

end;