let U1, U2 be non empty set ; :: thesis: for n being Nat
for E being Equivalence_Relation of U1
for F being Equivalence_Relation of U2
for g being b₁ -placesOf b₂,b₃ -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; :: thesis: for E being Equivalence_Relation of U1
for F being Equivalence_Relation of U2
for g being n -placesOf b₁,b₂ -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; :: thesis: for F being Equivalence_Relation of U2
for g being n -placesOf E,b₁ -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; :: thesis: 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; :: thesis: (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) ; :: thesis: verum