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

let x, z1, z2 be set ; :: thesis: ( [x,z1] in r3 * r4 & [x,z2] in r3 * r4 implies z1 = z2 )
assume C0: ( [x,z1] in r3 * r4 & [x,z2] in r3 * r4 ) ; :: thesis: z1 = z2
consider y1 being set such that
C1: ( [x,y1] in r3 & [y1,z1] in r4 ) by C0, RELAT_1:def 8;
consider y2 being set such that
C2: ( [x,y2] in r3 & [y2,z2] in r4 ) by C0, RELAT_1:def 8;
C8: ( f4 . y1 = z1 & f4 . y2 = z2 ) by C1, C2, FUNCT_1:1;
reconsider y11 = y1, y22 = y2 as Element of n -tuples_on U by C1, C2, ZFMISC_1:87;
consider p1 being Element of n -tuples_on (Class E), q1 being Element of n -tuples_on U such that
C4: ( [x,y1] = [p1,q1] & ( for j being set st j in Seg n holds
[(p1 . j),(q1 . j)] in r2 ) ) by C1;
consider p2 being Element of n -tuples_on (Class E), q2 being Element of n -tuples_on U such that
C5: ( [x,y2] = [p2,q2] & ( for j being set st j in Seg n holds
[(p2 . j),(q2 . j)] in r2 ) ) by C2;
C6: ( x = p1 & y1 = q1 & x = p2 & y2 = q2 ) by C4, C5, ZFMISC_1:27;
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

let j be set ; :: thesis: ( j in Seg n implies [(q1 . j),(q2 . j)] in E )
assume D1: 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 C4, C5, D1;
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 DefClass;
hence [(q1 . j),(q2 . j)] in E by C6, EQREL_1:35; :: thesis: verum

end;

then Z7: [y1,y2] in n -placesOf E by C6;
( ((n -placesOf E) -class) . y11 = Class ((n -placesOf E),y11) & ((n -placesOf E) -class) . y22 = Class ((n -placesOf E),y22) ) by DefClass;
hence z1 = z2 by Z7, C8, EQREL_1:35; :: thesis: verum

end;

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