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

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

hence
(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
by FUNCT_1:def 1; :: thesis: verumz1 = 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;

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

then A9:
[y1,y2] in n -placesOf E
by A7;[(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;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

( ((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