Metamath Proof Explorer

Theorem seqf1o

Description: Rearrange a sum via an arbitrary bijection on ( M ... N ) . (Contributed by Mario Carneiro, 27-Feb-2014) (Revised by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses seqf1o.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqf1o.2 
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
seqf1o.3 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqf1o.4 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqf1o.5 
|- ( ph -> C C_ S )
seqf1o.6 
|- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )
seqf1o.7 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( G ` x ) e. C )
seqf1o.8 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( G ` ( F ` k ) ) )
Assertion seqf1o 
|- ( ph -> ( seq M ( .+ , H ) ` N ) = ( seq M ( .+ , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqf1o.2 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqf1o.3 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqf1o.4 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqf1o.5 
 |-  ( ph -> C C_ S )
6 seqf1o.6 
 |-  ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )
7 seqf1o.7 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( G ` x ) e. C )
8 seqf1o.8 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( G ` ( F ` k ) ) )
9 7 fmpttd 
 |-  ( ph -> ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C )
10 oveq2 
 |-  ( x = M -> ( M ... x ) = ( M ... M ) )
11 f1oeq23 
 |-  ( ( ( M ... x ) = ( M ... M ) /\ ( M ... x ) = ( M ... M ) ) -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... M ) -1-1-onto-> ( M ... M ) ) )
12 10 10 11 syl2anc 
 |-  ( x = M -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... M ) -1-1-onto-> ( M ... M ) ) )
13 10 feq2d 
 |-  ( x = M -> ( g : ( M ... x ) --> C <-> g : ( M ... M ) --> C ) )
14 12 13 anbi12d 
 |-  ( x = M -> ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) <-> ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) )
15 fveq2 
 |-  ( x = M -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , ( g o. f ) ) ` M ) )
16 fveq2 
 |-  ( x = M -> ( seq M ( .+ , g ) ` x ) = ( seq M ( .+ , g ) ` M ) )
17 15 16 eqeq12d 
 |-  ( x = M -> ( ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) <-> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) )
18 14 17 imbi12d 
 |-  ( x = M -> ( ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) ) )
19 18 2albidv 
 |-  ( x = M -> ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) ) )
20 19 imbi2d 
 |-  ( x = M -> ( ( ph -> A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) ) <-> ( ph -> A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) ) ) )
21 oveq2 
 |-  ( x = k -> ( M ... x ) = ( M ... k ) )
22 f1oeq23 
 |-  ( ( ( M ... x ) = ( M ... k ) /\ ( M ... x ) = ( M ... k ) ) -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... k ) -1-1-onto-> ( M ... k ) ) )
23 21 21 22 syl2anc 
 |-  ( x = k -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... k ) -1-1-onto-> ( M ... k ) ) )
24 21 feq2d 
 |-  ( x = k -> ( g : ( M ... x ) --> C <-> g : ( M ... k ) --> C ) )
25 23 24 anbi12d 
 |-  ( x = k -> ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) <-> ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) ) )
26 fveq2 
 |-  ( x = k -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , ( g o. f ) ) ` k ) )
27 fveq2 
 |-  ( x = k -> ( seq M ( .+ , g ) ` x ) = ( seq M ( .+ , g ) ` k ) )
28 26 27 eqeq12d 
 |-  ( x = k -> ( ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) <-> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) )
29 25 28 imbi12d 
 |-  ( x = k -> ( ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) )
30 29 2albidv 
 |-  ( x = k -> ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) )
31 30 imbi2d 
 |-  ( x = k -> ( ( ph -> A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) ) <-> ( ph -> A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) ) )
32 oveq2 
 |-  ( x = ( k + 1 ) -> ( M ... x ) = ( M ... ( k + 1 ) ) )
33 f1oeq23 
 |-  ( ( ( M ... x ) = ( M ... ( k + 1 ) ) /\ ( M ... x ) = ( M ... ( k + 1 ) ) ) -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) ) )
34 32 32 33 syl2anc 
 |-  ( x = ( k + 1 ) -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) ) )
35 32 feq2d 
 |-  ( x = ( k + 1 ) -> ( g : ( M ... x ) --> C <-> g : ( M ... ( k + 1 ) ) --> C ) )
36 34 35 anbi12d 
 |-  ( x = ( k + 1 ) -> ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) <-> ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) )
37 fveq2 
 |-  ( x = ( k + 1 ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) )
38 fveq2 
 |-  ( x = ( k + 1 ) -> ( seq M ( .+ , g ) ` x ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) )
39 37 38 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) <-> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) )
40 36 39 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
41 40 2albidv 
 |-  ( x = ( k + 1 ) -> ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
42 41 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) ) <-> ( ph -> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) ) )
43 oveq2 
 |-  ( x = N -> ( M ... x ) = ( M ... N ) )
44 f1oeq23 
 |-  ( ( ( M ... x ) = ( M ... N ) /\ ( M ... x ) = ( M ... N ) ) -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
45 43 43 44 syl2anc 
 |-  ( x = N -> ( f : ( M ... x ) -1-1-onto-> ( M ... x ) <-> f : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
46 43 feq2d 
 |-  ( x = N -> ( g : ( M ... x ) --> C <-> g : ( M ... N ) --> C ) )
47 45 46 anbi12d 
 |-  ( x = N -> ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) <-> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) ) )
48 fveq2 
 |-  ( x = N -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , ( g o. f ) ) ` N ) )
49 fveq2 
 |-  ( x = N -> ( seq M ( .+ , g ) ` x ) = ( seq M ( .+ , g ) ` N ) )
50 48 49 eqeq12d 
 |-  ( x = N -> ( ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) <-> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) )
51 47 50 imbi12d 
 |-  ( x = N -> ( ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) ) )
52 51 2albidv 
 |-  ( x = N -> ( A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) <-> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) ) )
53 52 imbi2d 
 |-  ( x = N -> ( ( ph -> A. g A. f ( ( f : ( M ... x ) -1-1-onto-> ( M ... x ) /\ g : ( M ... x ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` x ) = ( seq M ( .+ , g ) ` x ) ) ) <-> ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) ) ) )
54 f1of 
 |-  ( f : ( M ... M ) -1-1-onto-> ( M ... M ) -> f : ( M ... M ) --> ( M ... M ) )
55 54 adantr 
 |-  ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> f : ( M ... M ) --> ( M ... M ) )
56 elfz3 
 |-  ( M e. ZZ -> M e. ( M ... M ) )
57 fvco3 
 |-  ( ( f : ( M ... M ) --> ( M ... M ) /\ M e. ( M ... M ) ) -> ( ( g o. f ) ` M ) = ( g ` ( f ` M ) ) )
58 55 56 57 syl2anr 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( ( g o. f ) ` M ) = ( g ` ( f ` M ) ) )
59 ffvelrn 
 |-  ( ( f : ( M ... M ) --> ( M ... M ) /\ M e. ( M ... M ) ) -> ( f ` M ) e. ( M ... M ) )
60 54 56 59 syl2anr 
 |-  ( ( M e. ZZ /\ f : ( M ... M ) -1-1-onto-> ( M ... M ) ) -> ( f ` M ) e. ( M ... M ) )
61 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
62 61 eleq2d 
 |-  ( M e. ZZ -> ( ( f ` M ) e. ( M ... M ) <-> ( f ` M ) e. { M } ) )
63 elsni 
 |-  ( ( f ` M ) e. { M } -> ( f ` M ) = M )
64 62 63 syl6bi 
 |-  ( M e. ZZ -> ( ( f ` M ) e. ( M ... M ) -> ( f ` M ) = M ) )
65 64 imp 
 |-  ( ( M e. ZZ /\ ( f ` M ) e. ( M ... M ) ) -> ( f ` M ) = M )
66 60 65 syldan 
 |-  ( ( M e. ZZ /\ f : ( M ... M ) -1-1-onto-> ( M ... M ) ) -> ( f ` M ) = M )
67 66 adantrr 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( f ` M ) = M )
68 67 fveq2d 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( g ` ( f ` M ) ) = ( g ` M ) )
69 58 68 eqtrd 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( ( g o. f ) ` M ) = ( g ` M ) )
70 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( ( g o. f ) ` M ) )
71 70 adantr 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( ( g o. f ) ` M ) )
72 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , g ) ` M ) = ( g ` M ) )
73 72 adantr 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( seq M ( .+ , g ) ` M ) = ( g ` M ) )
74 69 71 73 3eqtr4d 
 |-  ( ( M e. ZZ /\ ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) )
75 74 ex 
 |-  ( M e. ZZ -> ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) )
76 75 alrimivv 
 |-  ( M e. ZZ -> A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) )
77 76 a1d 
 |-  ( M e. ZZ -> ( ph -> A. g A. f ( ( f : ( M ... M ) -1-1-onto-> ( M ... M ) /\ g : ( M ... M ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` M ) = ( seq M ( .+ , g ) ` M ) ) ) )
78 f1oeq1 
 |-  ( f = t -> ( f : ( M ... k ) -1-1-onto-> ( M ... k ) <-> t : ( M ... k ) -1-1-onto-> ( M ... k ) ) )
79 feq1 
 |-  ( g = s -> ( g : ( M ... k ) --> C <-> s : ( M ... k ) --> C ) )
80 78 79 bi2anan9r 
 |-  ( ( g = s /\ f = t ) -> ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) <-> ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) ) )
81 coeq1 
 |-  ( g = s -> ( g o. f ) = ( s o. f ) )
82 coeq2 
 |-  ( f = t -> ( s o. f ) = ( s o. t ) )
83 81 82 sylan9eq 
 |-  ( ( g = s /\ f = t ) -> ( g o. f ) = ( s o. t ) )
84 83 seqeq3d 
 |-  ( ( g = s /\ f = t ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( s o. t ) ) )
85 84 fveq1d 
 |-  ( ( g = s /\ f = t ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , ( s o. t ) ) ` k ) )
86 simpl 
 |-  ( ( g = s /\ f = t ) -> g = s )
87 86 seqeq3d 
 |-  ( ( g = s /\ f = t ) -> seq M ( .+ , g ) = seq M ( .+ , s ) )
88 87 fveq1d 
 |-  ( ( g = s /\ f = t ) -> ( seq M ( .+ , g ) ` k ) = ( seq M ( .+ , s ) ` k ) )
89 85 88 eqeq12d 
 |-  ( ( g = s /\ f = t ) -> ( ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) <-> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) )
90 80 89 imbi12d 
 |-  ( ( g = s /\ f = t ) -> ( ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) <-> ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) ) )
91 90 cbval2vw 
 |-  ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) <-> A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) )
92 simplll 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> ph )
93 92 1 sylan 
 |-  ( ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
94 92 2 sylan 
 |-  ( ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
95 92 3 sylan 
 |-  ( ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
96 simpllr 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> k e. ( ZZ>= ` M ) )
97 92 5 syl 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> C C_ S )
98 simprl 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) )
99 simprr 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> g : ( M ... ( k + 1 ) ) --> C )
100 eqid 
 |-  ( w e. ( M ... k ) |-> ( f ` if ( w < ( `' f ` ( k + 1 ) ) , w , ( w + 1 ) ) ) ) = ( w e. ( M ... k ) |-> ( f ` if ( w < ( `' f ` ( k + 1 ) ) , w , ( w + 1 ) ) ) )
101 eqid 
 |-  ( `' f ` ( k + 1 ) ) = ( `' f ` ( k + 1 ) )
102 simplr 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) )
103 102 91 sylib 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) )
104 93 94 95 96 97 98 99 100 101 103 seqf1olem2 
 |-  ( ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) /\ ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) )
105 104 exp31 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) -> ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
106 91 105 syl5bir 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) -> ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
107 106 alrimdv 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) -> A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
108 107 alrimdv 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A. s A. t ( ( t : ( M ... k ) -1-1-onto-> ( M ... k ) /\ s : ( M ... k ) --> C ) -> ( seq M ( .+ , ( s o. t ) ) ` k ) = ( seq M ( .+ , s ) ` k ) ) -> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
109 91 108 syl5bi 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) -> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) )
110 109 expcom 
 |-  ( k e. ( ZZ>= ` M ) -> ( ph -> ( A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) -> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) ) )
111 110 a2d 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ph -> A. g A. f ( ( f : ( M ... k ) -1-1-onto-> ( M ... k ) /\ g : ( M ... k ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` k ) = ( seq M ( .+ , g ) ` k ) ) ) -> ( ph -> A. g A. f ( ( f : ( M ... ( k + 1 ) ) -1-1-onto-> ( M ... ( k + 1 ) ) /\ g : ( M ... ( k + 1 ) ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` ( k + 1 ) ) = ( seq M ( .+ , g ) ` ( k + 1 ) ) ) ) ) )
112 20 31 42 53 77 111 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) ) )
113 4 112 mpcom 
 |-  ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) )
114 fvex 
 |-  ( G ` x ) e. _V
115 eqid 
 |-  ( x e. ( M ... N ) |-> ( G ` x ) ) = ( x e. ( M ... N ) |-> ( G ` x ) )
116 114 115 fnmpti 
 |-  ( x e. ( M ... N ) |-> ( G ` x ) ) Fn ( M ... N )
117 fzfi 
 |-  ( M ... N ) e. Fin
118 fnfi 
 |-  ( ( ( x e. ( M ... N ) |-> ( G ` x ) ) Fn ( M ... N ) /\ ( M ... N ) e. Fin ) -> ( x e. ( M ... N ) |-> ( G ` x ) ) e. Fin )
119 116 117 118 mp2an 
 |-  ( x e. ( M ... N ) |-> ( G ` x ) ) e. Fin
120 f1of 
 |-  ( F : ( M ... N ) -1-1-onto-> ( M ... N ) -> F : ( M ... N ) --> ( M ... N ) )
121 6 120 syl 
 |-  ( ph -> F : ( M ... N ) --> ( M ... N ) )
122 ovexd 
 |-  ( ph -> ( M ... N ) e. _V )
123 fex2 
 |-  ( ( F : ( M ... N ) --> ( M ... N ) /\ ( M ... N ) e. _V /\ ( M ... N ) e. _V ) -> F e. _V )
124 121 122 122 123 syl3anc 
 |-  ( ph -> F e. _V )
125 f1oeq1 
 |-  ( f = F -> ( f : ( M ... N ) -1-1-onto-> ( M ... N ) <-> F : ( M ... N ) -1-1-onto-> ( M ... N ) ) )
126 feq1 
 |-  ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) -> ( g : ( M ... N ) --> C <-> ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) )
127 125 126 bi2anan9r 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) <-> ( F : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) ) )
128 coeq1 
 |-  ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) -> ( g o. f ) = ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. f ) )
129 coeq2 
 |-  ( f = F -> ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. f ) = ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) )
130 128 129 sylan9eq 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( g o. f ) = ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) )
131 130 seqeq3d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> seq M ( .+ , ( g o. f ) ) = seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) )
132 131 fveq1d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) )
133 simpl 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> g = ( x e. ( M ... N ) |-> ( G ` x ) ) )
134 133 seqeq3d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> seq M ( .+ , g ) = seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) )
135 134 fveq1d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( seq M ( .+ , g ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) )
136 132 135 eqeq12d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) <-> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) ) )
137 127 136 imbi12d 
 |-  ( ( g = ( x e. ( M ... N ) |-> ( G ` x ) ) /\ f = F ) -> ( ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) <-> ( ( F : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) ) ) )
138 137 spc2gv 
 |-  ( ( ( x e. ( M ... N ) |-> ( G ` x ) ) e. Fin /\ F e. _V ) -> ( A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) -> ( ( F : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) ) ) )
139 119 124 138 sylancr 
 |-  ( ph -> ( A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) -> ( ( F : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) ) ) )
140 113 139 mpd 
 |-  ( ph -> ( ( F : ( M ... N ) -1-1-onto-> ( M ... N ) /\ ( x e. ( M ... N ) |-> ( G ` x ) ) : ( M ... N ) --> C ) -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) ) )
141 6 9 140 mp2and 
 |-  ( ph -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) )
142 121 ffvelrnda 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. ( M ... N ) )
143 fveq2 
 |-  ( x = ( F ` k ) -> ( G ` x ) = ( G ` ( F ` k ) ) )
144 fvex 
 |-  ( G ` ( F ` k ) ) e. _V
145 143 115 144 fvmpt 
 |-  ( ( F ` k ) e. ( M ... N ) -> ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` ( F ` k ) ) = ( G ` ( F ` k ) ) )
146 142 145 syl 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` ( F ` k ) ) = ( G ` ( F ` k ) ) )
147 fvco3 
 |-  ( ( F : ( M ... N ) --> ( M ... N ) /\ k e. ( M ... N ) ) -> ( ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ` k ) = ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` ( F ` k ) ) )
148 121 147 sylan 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ` k ) = ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` ( F ` k ) ) )
149 146 148 8 3eqtr4d 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ` k ) = ( H ` k ) )
150 4 149 seqfveq 
 |-  ( ph -> ( seq M ( .+ , ( ( x e. ( M ... N ) |-> ( G ` x ) ) o. F ) ) ` N ) = ( seq M ( .+ , H ) ` N ) )
151 fveq2 
 |-  ( x = k -> ( G ` x ) = ( G ` k ) )
152 fvex 
 |-  ( G ` k ) e. _V
153 151 115 152 fvmpt 
 |-  ( k e. ( M ... N ) -> ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` k ) = ( G ` k ) )
154 153 adantl 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( x e. ( M ... N ) |-> ( G ` x ) ) ` k ) = ( G ` k ) )
155 4 154 seqfveq 
 |-  ( ph -> ( seq M ( .+ , ( x e. ( M ... N ) |-> ( G ` x ) ) ) ` N ) = ( seq M ( .+ , G ) ` N ) )
156 141 150 155 3eqtr3d 
 |-  ( ph -> ( seq M ( .+ , H ) ` N ) = ( seq M ( .+ , G ) ` N ) )