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 :: thesis: for x, y1, y2 being object st [x,y1] in n -placesOf f & [x,y2] in n -placesOf f holds
y1 = y2

let x, y1, y2 be object ; :: 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
A1: ( [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
A2: ( [x,y2] = [p2,q2] & ( for j being set st j in Seg n holds
[(p2 . j),(q2 . j)] in f ) ) ;
A3: ( x = p1 & y1 = q1 & x = p2 & y2 = q2 ) by A1, A2, XTUPLE_0:1;
reconsider xx = x as Function by A2, XTUPLE_0:1;
reconsider qq1 = q1, qq2 = q2 as Element of Funcs ((Seg n),U2) by FOMODEL0:11;

now :: thesis: for j being Element of Seg n holds qq1 . j = qq2 . j

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 A1, A2, A3;
hence qq1 . j = qq2 . j by FUNCT_1:def 1; :: thesis: verum

end;

hence y1 = y2 by A3, 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;