let n be Nat; :: thesis: for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds
rng p1 c= rng p2
let p1, p2 be one-to-one a_partition of n; :: thesis: ( Euler_transformation p1 = Euler_transformation p2 implies rng p1 c= rng p2 )
assume A1: Euler_transformation p1 = Euler_transformation p2 ; :: thesis: rng p1 c= rng p2
consider O1 being odd-valued FinSequence, a1 being natural-valued FinSequence such that
A2: ( len O1 = len p1 & len p1 = len a1 & p1 = O1 (#) (2 |^ a1) ) and
A3: p1 . 1 = (O1 . 1) * (2 |^ (a1 . 1)) & ... & p1 . (len p1) = (O1 . (len p1)) * (2 |^ (a1 . (len p1))) by Th6;
set s1 = the odd_organization of O1;
reconsider S1 = the odd_organization of O1 as DoubleReorganization of dom a1 by FINSEQ_3:29, A2;
consider O2 being odd-valued FinSequence, a2 being natural-valued FinSequence such that
A4: ( len O2 = len p2 & len p2 = len a2 & p2 = O2 (#) (2 |^ a2) ) and
A5: p2 . 1 = (O2 . 1) * (2 |^ (a2 . 1)) & ... & p2 . (len p2) = (O2 . (len p2)) * (2 |^ (a2 . (len p2))) by Th6;
set s2 = the odd_organization of O2;
reconsider S2 = the odd_organization of O2 as DoubleReorganization of dom a2 by FINSEQ_3:29, A4;
A6: for j being Nat holds rng ((a1 *. the odd_organization of O1) . j) = rng ((a2 *. the odd_organization of O2) . j)

proof

let j be Nat; :: thesis: rng ((a1 *. the odd_organization of O1) . j) = rng ((a2 *. the odd_organization of O2) . j)
A7: card (Coim ((Euler_transformation p1),((j * 2) - 1))) = ((((2 |^ a1) *. the odd_organization of O1) . j),1) +... by A2, Th12
.= (((2 |^ a1) * ( the odd_organization of O1 . j)),1) +... by FLEXARY1:41
.= ((2 |^ (a1 * ( the odd_organization of O1 . j))),1) +... by FLEXARY1:25
.= ((2 |^ (a1 * (S1 . j))) . 1) + (((2 |^ (a1 * (S1 . j))),(1 + 1)) +...) by FLEXARY1:20 ;
A8: (a2 *. S2) . j = a2 * (S2 . j) by FLEXARY1:41;
then A9: ( a2 * (S2 . j) is one-to-one & a2 * (S2 . j) is natural-valued ) by A4, Th13;
(a1 *. S1) . j = a1 * (S1 . j) by FLEXARY1:41;
then A10: ( a1 * (S1 . j) is one-to-one & a1 * (S1 . j) is natural-valued ) by A2, Th13;
card (Coim ((Euler_transformation p2),((j * 2) - 1))) = ((((2 |^ a2) *. the odd_organization of O2) . j),1) +... by A4, Th12
.= (((2 |^ a2) * ( the odd_organization of O2 . j)),1) +... by FLEXARY1:41
.= ((2 |^ (a2 * ( the odd_organization of O2 . j))),1) +... by FLEXARY1:25
.= ((2 |^ (a2 * (S2 . j))) . 1) + (((2 |^ (a2 * (S2 . j))),(1 + 1)) +...) by FLEXARY1:20 ;
then rng (a2 * (S2 . j)) = rng (a1 * (S1 . j)) by A7, A1, FLEXARY1:30, A9, A10;
hence rng ((a1 *. the odd_organization of O1) . j) = rng ((a2 *. the odd_organization of O2) . j) by A8, FLEXARY1:41; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p1 or y in rng p2 )
assume y in rng p1 ; :: thesis: y in rng p2
then consider x being object such that
A11: ( x in dom p1 & p1 . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A11;
( 1 <= x & x <= len p1 ) by A11, FINSEQ_3:25;
then A12: p1 . x = (O1 . x) * (2 |^ (a1 . x)) by A3;
dom p1 = dom O1 by A2, FINSEQ_3:29;
then x in Values the odd_organization of O1 by FLEXARY1:def 7, A11;
then consider i, j being object such that
A13: ( i in dom the odd_organization of O1 & j in dom ( the odd_organization of O1 . i) & x = ( the odd_organization of O1 . i) . j ) by FLEXARY1:1;
reconsider i = i, j = j as Nat by A13;
len ((a1 *. S1) . i) = len (S1 . i) by CARD_1:def 7;
then A14: dom ((a1 *. S1) . i) = dom (S1 . i) by FINSEQ_3:29;
then ((a1 *. S1) . i) . j in rng ((a1 *. the odd_organization of O1) . i) by A13, FUNCT_1:def 3;
then ((a1 *. S1) . i) . j in rng ((a2 *. the odd_organization of O2) . i) by A6;
then consider z being object such that
A15: ( z in dom ((a2 *. S2) . i) & ((a2 *. S2) . i) . z = ((a1 *. S1) . i) . j ) by FUNCT_1:def 3;
reconsider z = z as Nat by A15;
set Z = (S2 . i) . z;
A16: (a1 *. S1) . i = a1 * (S1 . i) by FLEXARY1:41;
A17: (a2 *. S2) . i = a2 * (S2 . i) by FLEXARY1:41;
A18: len ((a2 *. S2) . i) = len (S2 . i) by CARD_1:def 7;
A19: ( ((a2 *. S2) . i) . z = a2 . ((S2 . i) . z) & (S2 . i) . z in dom a2 ) by A17, A15, FUNCT_1:11, FUNCT_1:12;
then A20: (S2 . i) . z in dom p2 by FINSEQ_3:29, A4;
( 1 <= (S2 . i) . z & (S2 . i) . z <= len p2 ) by A19, A4, FINSEQ_3:25;
then A21: p2 . ((S2 . i) . z) = (O2 . ((S2 . i) . z)) * (2 |^ (a2 . ((S2 . i) . z))) by A5;
A22: p2 . ((S2 . i) . z) in rng p2 by A20, FUNCT_1:def 3;
A23: ( 1 <= j & j <= len ( the odd_organization of O1 . i) ) by A13, FINSEQ_3:25;
(2 * i) - 1 = O1 . ( the odd_organization of O1 _ (i,1)) & ... & (2 * i) - 1 = O1 . ( the odd_organization of O1 _ (i,(len ( the odd_organization of O1 . i)))) by Def4;
then A24: O1 . ( the odd_organization of O1 _ (i,j)) = (2 * i) - 1 by A23;
A25: ( 1 <= z & z <= len ( the odd_organization of O2 . i) ) by FINSEQ_3:25, A18, A15;
(2 * i) - 1 = O2 . ( the odd_organization of O2 _ (i,1)) & ... & (2 * i) - 1 = O2 . ( the odd_organization of O2 _ (i,(len ( the odd_organization of O2 . i)))) by Def4;
then O2 . ( the odd_organization of O2 _ (i,z)) = (2 * i) - 1 by A25;
hence y in rng p2 by A24, A13, A22, A21, A15, A16, A14, FUNCT_1:12, A19, A12, A11; :: thesis: verum