let U1, U2 be non empty set ; for n being Nat
for E being Equivalence_Relation of U1
for F being Equivalence_Relation of U2
for g being b1 -placesOf b2,b3 -respecting Function of (n -tuples_on U1),U2 holds (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
let n be Nat; for E being Equivalence_Relation of U1
for F being Equivalence_Relation of U2
for g being n -placesOf b1,b2 -respecting Function of (n -tuples_on U1),U2 holds (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
set X = U1;
set Y = U2;
let E be Equivalence_Relation of U1; for F being Equivalence_Relation of U2
for g being n -placesOf E,b1 -respecting Function of (n -tuples_on U1),U2 holds (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
let F be Equivalence_Relation of U2; for g being n -placesOf E,F -respecting Function of (n -tuples_on U1),U2 holds (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
let g be n -placesOf E,F -respecting Function of (n -tuples_on U1),U2; (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
reconsider G = g quotient ((n -placesOf E),F) as Function of (Class (n -placesOf E)),(Class F) ;
reconsider R = G as Relation of (Class (n -placesOf E)),(Class F) ;
reconsider projector = E -class as Relation of U1,(Class E) ;
G * (n -tuple2Class E) =
(n -placesOf (projector ~)) * (((n -placesOf E) -class) * R)
by RELAT_1:36
.=
(n -placesOf (projector ~)) * ((F -class) * g)
by Lm18
;
hence
(g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
; verum