set IT = n -placesOf f;

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

end;

suppose
n = 0
; :: thesis: for b_{1} being Relation st b_{1} = n -placesOf f holds

b_{1} is Function-like

b

hence
for b_{1} being Relation st b_{1} = n -placesOf f holds

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

end;b

suppose
n <> 0
; :: thesis: for b_{1} being Relation st b_{1} = n -placesOf f holds

b_{1} is Function-like

b

then reconsider n = n as non zero Nat ;

_{1} being Relation st b_{1} = n -placesOf f holds

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

end;now :: thesis: for x, y1, y2 being object st [x,y1] in n -placesOf f & [x,y2] in n -placesOf f holds

y1 = y2

hence
for by1 = 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;

end;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

hence
y1 = y2
by A3, FUNCT_2:63; :: thesis: verumlet 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;( [(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

b