let n be Nat; 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; ( Euler_transformation p1 = Euler_transformation p2 implies rng p1 c= rng p2 )
assume A1:
Euler_transformation p1 = Euler_transformation p2
; 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;
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;
verum
end;
let y be object ; TARSKI:def 3 ( not y in rng p1 or y in rng p2 )
assume
y in rng p1
; 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; verum