let U be non empty set ; :: thesis: for E being Equivalence_Relation of U
for n being non zero Nat holds (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
let E be Equivalence_Relation of U; :: thesis: for n being non zero Nat holds (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
let n be non zero Nat; :: thesis: (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
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 r3 = n -placesOf r2 as Relation of (n -tuples_on (Class E)),(n -tuples_on U) ;
reconsider f4 = (n -placesOf E) -class as Function of (n -tuples_on U),(Class (n -placesOf E)) ;
reconsider r4 = f4 as Relation of (n -tuples_on U),(Class (n -placesOf E)) ;

now :: thesis: for x, z1, z2 being object st [x,z1] in r3 * r4 & [x,z2] in r3 * r4 holds
z1 = z2

let x, z1, z2 be object ; :: thesis: ( [x,z1] in r3 * r4 & [x,z2] in r3 * r4 implies z1 = z2 )
assume A1: ( [x,z1] in r3 * r4 & [x,z2] in r3 * r4 ) ; :: thesis: z1 = z2
consider y1 being object such that
A2: ( [x,y1] in r3 & [y1,z1] in r4 ) by A1, RELAT_1:def 8;
consider y2 being object such that
A3: ( [x,y2] in r3 & [y2,z2] in r4 ) by A1, RELAT_1:def 8;
A4: ( f4 . y1 = z1 & f4 . y2 = z2 ) by FUNCT_1:1, A2, A3;
reconsider y11 = y1, y22 = y2 as Element of n -tuples_on U by ZFMISC_1:87, A2, A3;
consider p1 being Element of n -tuples_on (Class E), q1 being Element of n -tuples_on U such that
A5: ( [x,y1] = [p1,q1] & ( for j being set st j in Seg n holds
[(p1 . j),(q1 . j)] in r2 ) ) by A2;
consider p2 being Element of n -tuples_on (Class E), q2 being Element of n -tuples_on U such that
A6: ( [x,y2] = [p2,q2] & ( for j being set st j in Seg n holds
[(p2 . j),(q2 . j)] in r2 ) ) by A3;
A7: ( x = p1 & y1 = q1 & x = p2 & y2 = q2 ) by XTUPLE_0:1, A5, A6;
reconsider q11 = q1 as Element of Funcs ((Seg n),U) by FOMODEL0:11;
reconsider q22 = q2 as Element of Funcs ((Seg n),U) by FOMODEL0:11;

now :: thesis: for j being set st j in Seg n holds
[(q1 . j),(q2 . j)] in E

let j be set ; :: thesis: ( j in Seg n implies [(q1 . j),(q2 . j)] in E )
assume A8: j in Seg n ; :: thesis: [(q1 . j),(q2 . j)] in E
then reconsider jj = j as Element of Seg n ;
( [(p1 . j),(q1 . j)] in r2 & [(p2 . j),(q2 . j)] in r2 ) by A5, A6, A8;
then ( [(q1 . j),(p1 . j)] in f1 & [(q2 . j),(p2 . j)] in f1 ) by RELAT_1:def 7;
then ( f1 . (q1 . jj) = p1 . jj & f1 . (q2 . jj) = p2 . jj ) by FUNCT_1:1;
then ( Class (E,(q11 . jj)) = p1 . jj & Class (E,(q22 . jj)) = p2 . jj ) by Def13;
hence [(q1 . j),(q2 . j)] in E by A7, EQREL_1:35; :: thesis: verum

end;

then A9: [y1,y2] in n -placesOf E by A7;
( ((n -placesOf E) -class) . y11 = Class ((n -placesOf E),y11) & ((n -placesOf E) -class) . y22 = Class ((n -placesOf E),y22) ) by Def13;
hence z1 = z2 by A9, EQREL_1:35, A4; :: thesis: verum

end;

hence (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like by FUNCT_1:def 1; :: thesis: verum