set IT = n -placesOf f;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: for b₁ being Relation st b₁ = n -placesOf f holds
b₁ is Function-like

hence for b₁ being Relation st b₁ = n -placesOf f holds
b₁ is Function-like ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: for b₁ being Relation st b₁ = n -placesOf f holds
b₁ is Function-like

then reconsider n = n as non zero Nat ;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in n -placesOf f & [x,y2] in n -placesOf f implies y1 = y2 )
assume [x,y1] in n -placesOf f ; :: thesis: ( [x,y2] in n -placesOf f implies y1 = y2 )
then consider p1 being Element of n -tuples_on U1, q1 being Element of n -tuples_on U2 such that
C1: ( [x,y1] = [p1,q1] & ( for j being set st j in Seg n holds
[(p1 . j),(q1 . j)] in f ) ) ;
assume [x,y2] in n -placesOf f ; :: thesis: y1 = y2
then consider p2 being Element of n -tuples_on U1, q2 being Element of n -tuples_on U2 such that
C2: ( [x,y2] = [p2,q2] & ( for j being set st j in Seg n holds
[(p2 . j),(q2 . j)] in f ) ) ;
C3: ( x = p1 & y1 = q1 & x = p2 & y2 = q2 ) by C1, C2, ZFMISC_1:27;
reconsider xx = x as Function by C2, ZFMISC_1:27;
reconsider qq1 = q1, qq2 = q2 as Element of Funcs ((Seg n),U2) by FOMODEL0:11;

now

let j be Element of Seg n; :: thesis: qq1 . j = qq2 . j
( [(xx . j),(q1 . j)] in f & [(xx . j),(q2 . j)] in f ) by C1, C2, C3;
hence qq1 . j = qq2 . j by FUNCT_1:def 1; :: thesis: verum

end;

hence y1 = y2 by C3, FUNCT_2:63; :: thesis: verum

end;

hence for b₁ being Relation st b₁ = n -placesOf f holds
b₁ is Function-like by FUNCT_1:def 1; :: thesis: verum

end;

end;