let n be Nat; :: thesis: for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds
p1 = p2
let p1, p2 be one-to-one a_partition of n; :: thesis: ( Euler_transformation p1 = Euler_transformation p2 implies p1 = p2 )
assume Euler_transformation p1 = Euler_transformation p2 ; :: thesis: p1 = p2
then A1: rng p1 = rng p2 by Lm4;
then ( p1 is FinSequence of REAL & p2 is FinSequence of REAL ) by FINSEQ_1:def 4;
hence p1 = p2 by INTEGRA3:6, A1; :: thesis: verum