let U be non empty set ; :: thesis: for n being Nat
for E being Equivalence_Relation of U holds (n -placesOf E) -class = (n -tuple2Class E) * (n -placesOf (E -class))
let n be Nat; :: thesis: for E being Equivalence_Relation of U holds (n -placesOf E) -class = (n -tuple2Class E) * (n -placesOf (E -class))
let E be Equivalence_Relation of U; :: thesis: (n -placesOf E) -class = (n -tuple2Class E) * (n -placesOf (E -class))
set UN = n -tuples_on U;
set A = n -tuple2Class E;
set RH = (n -tuple2Class E) * (n -placesOf (E -class));
set LH = (n -placesOf E) -class ;
reconsider RA = n -placesOf (E -class) as Relation of (n -tuples_on U),(n -tuples_on (Class E)) ;
reconsider ER = E -class as Relation of U,(Class E) ;
reconsider RB = n -placesOf (ER ~) as Relation of (n -tuples_on (Class E)),(n -tuples_on U) ;
reconsider RC = (n -placesOf ER) ~ as Relation of (n -tuples_on (Class E)),(n -tuples_on U) ;
A1: ( dom ((n -placesOf E) -class) = n -tuples_on U & dom ((n -tuple2Class E) * (n -placesOf (E -class))) = n -tuples_on U ) by FUNCT_2:def 1;
reconsider FA = RA as Function of (n -tuples_on U),(n -tuples_on (Class E)) ;
reconsider RAA = RA as n -tuples_on U -defined total Relation ;
(n -tuple2Class E) * (n -placesOf (E -class)) = (RA * RB) * ((n -placesOf E) -class) by RELAT_1:36
.= (RA * RC) * ((n -placesOf E) -class) by Lm17 ;
then (id (n -tuples_on U)) * ((n -placesOf E) -class) c= (n -tuple2Class E) * (n -placesOf (E -class)) by FOMODEL0:21, RELAT_1:30;
then ((n -placesOf E) -class) | (n -tuples_on U) c= (n -tuple2Class E) * (n -placesOf (E -class)) by RELAT_1:65;
hence (n -placesOf E) -class = (n -tuple2Class E) * (n -placesOf (E -class)) by GRFUNC_1:3, A1; :: thesis: verum