per cases ( not n is zero or n is zero ) ;
suppose not n is zero ; :: thesis: for b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 is Function-like
hence for b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 is Function-like by Lm11; :: thesis: verum
end;
suppose n is zero ; :: thesis: for b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 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 b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 is Function-like ; :: thesis: verum
end;
end;