let U be non empty set ; 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; for n being non zero Nat holds (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
let n be non zero Nat; (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 for x, z1, z2 being object st [x,z1] in r3 * r4 & [x,z2] in r3 * r4 holds
z1 = z2let x,
z1,
z2 be
object ;
( [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 )
;
z1 = z2consider 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 for j being set st j in Seg n holds
[(q1 . j),(q2 . j)] in Elet j be
set ;
( j in Seg n implies [(q1 . j),(q2 . j)] in E )assume A8:
j in Seg n
;
[(q1 . j),(q2 . j)] in Ethen 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;
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;
verum end;
hence
(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
by FUNCT_1:def 1; verum