Metamath Proof Explorer

Theorem fmuldfeqlem1

Description: induction step for the proof of fmuldfeq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmuldfeqlem1.1 
|- F/ f ph
fmuldfeqlem1.2 
|- F/ g ph
fmuldfeqlem1.3 
|- F/_ t Y
fmuldfeqlem1.5 
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
fmuldfeqlem1.6 
|- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
fmuldfeqlem1.7 
|- ( ph -> T e. _V )
fmuldfeqlem1.8 
|- ( ph -> U : ( 1 ... M ) --> Y )
fmuldfeqlem1.9 
|- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
fmuldfeqlem1.10 
|- ( ph -> N e. ( 1 ... M ) )
fmuldfeqlem1.11 
|- ( ph -> ( N + 1 ) e. ( 1 ... M ) )
fmuldfeqlem1.12 
|- ( ph -> ( ( seq 1 ( P , U ) ` N ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` N ) )
fmuldfeqlem1.13 
|- ( ( ph /\ f e. Y ) -> f : T --> RR )
Assertion fmuldfeqlem1 
|- ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 fmuldfeqlem1.1 
 |-  F/ f ph
2 fmuldfeqlem1.2 
 |-  F/ g ph
3 fmuldfeqlem1.3 
 |-  F/_ t Y
4 fmuldfeqlem1.5 
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
5 fmuldfeqlem1.6 
 |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
6 fmuldfeqlem1.7 
 |-  ( ph -> T e. _V )
7 fmuldfeqlem1.8 
 |-  ( ph -> U : ( 1 ... M ) --> Y )
8 fmuldfeqlem1.9 
 |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
9 fmuldfeqlem1.10 
 |-  ( ph -> N e. ( 1 ... M ) )
10 fmuldfeqlem1.11 
 |-  ( ph -> ( N + 1 ) e. ( 1 ... M ) )
11 fmuldfeqlem1.12 
 |-  ( ph -> ( ( seq 1 ( P , U ) ` N ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` N ) )
12 fmuldfeqlem1.13 
 |-  ( ( ph /\ f e. Y ) -> f : T --> RR )
13 ovex 
 |-  ( 1 ... M ) e. _V
14 13 mptex 
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V
15 5 fvmpt2 
 |-  ( ( t e. T /\ ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
16 14 15 mpan2 
 |-  ( t e. T -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )
17 fveq2 
 |-  ( i = j -> ( U ` i ) = ( U ` j ) )
18 17 fveq1d 
 |-  ( i = j -> ( ( U ` i ) ` t ) = ( ( U ` j ) ` t ) )
19 18 cbvmptv 
 |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) )
20 16 19 eqtrdi 
 |-  ( t e. T -> ( F ` t ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) ) )
21 20 adantl 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) = ( j e. ( 1 ... M ) |-> ( ( U ` j ) ` t ) ) )
22 fveq2 
 |-  ( j = ( N + 1 ) -> ( U ` j ) = ( U ` ( N + 1 ) ) )
23 22 fveq1d 
 |-  ( j = ( N + 1 ) -> ( ( U ` j ) ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
24 23 adantl 
 |-  ( ( ( ph /\ t e. T ) /\ j = ( N + 1 ) ) -> ( ( U ` j ) ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
25 10 adantr 
 |-  ( ( ph /\ t e. T ) -> ( N + 1 ) e. ( 1 ... M ) )
26 7 10 ffvelcdmd 
 |-  ( ph -> ( U ` ( N + 1 ) ) e. Y )
27 26 ancli 
 |-  ( ph -> ( ph /\ ( U ` ( N + 1 ) ) e. Y ) )
28 nfcv 
 |-  F/_ f ( U ` ( N + 1 ) )
29 nfv 
 |-  F/ f ( U ` ( N + 1 ) ) e. Y
30 1 29 nfan 
 |-  F/ f ( ph /\ ( U ` ( N + 1 ) ) e. Y )
31 nfv 
 |-  F/ f ( U ` ( N + 1 ) ) : T --> RR
32 30 31 nfim 
 |-  F/ f ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR )
33 eleq1 
 |-  ( f = ( U ` ( N + 1 ) ) -> ( f e. Y <-> ( U ` ( N + 1 ) ) e. Y ) )
34 33 anbi2d 
 |-  ( f = ( U ` ( N + 1 ) ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( U ` ( N + 1 ) ) e. Y ) ) )
35 feq1 
 |-  ( f = ( U ` ( N + 1 ) ) -> ( f : T --> RR <-> ( U ` ( N + 1 ) ) : T --> RR ) )
36 34 35 imbi12d 
 |-  ( f = ( U ` ( N + 1 ) ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR ) ) )
37 28 32 36 12 vtoclgf 
 |-  ( ( U ` ( N + 1 ) ) e. Y -> ( ( ph /\ ( U ` ( N + 1 ) ) e. Y ) -> ( U ` ( N + 1 ) ) : T --> RR ) )
38 26 27 37 sylc 
 |-  ( ph -> ( U ` ( N + 1 ) ) : T --> RR )
39 38 ffvelcdmda 
 |-  ( ( ph /\ t e. T ) -> ( ( U ` ( N + 1 ) ) ` t ) e. RR )
40 21 24 25 39 fvmptd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` ( N + 1 ) ) = ( ( U ` ( N + 1 ) ) ` t ) )
41 40 oveq2d 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
42 elfzuz 
 |-  ( N e. ( 1 ... M ) -> N e. ( ZZ>= ` 1 ) )
43 9 42 syl 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
44 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
45 43 44 syl 
 |-  ( ph -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
46 45 adantr 
 |-  ( ( ph /\ t e. T ) -> ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( F ` t ) ` ( N + 1 ) ) ) )
47 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) )
48 43 47 syl 
 |-  ( ph -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) )
49 nfcv 
 |-  F/_ h ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
50 nfcv 
 |-  F/_ l ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
51 nfcv 
 |-  F/_ f ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) )
52 nfcv 
 |-  F/_ g ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) )
53 fveq1 
 |-  ( f = h -> ( f ` t ) = ( h ` t ) )
54 fveq1 
 |-  ( g = l -> ( g ` t ) = ( l ` t ) )
55 53 54 oveqan12d 
 |-  ( ( f = h /\ g = l ) -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
56 55 mpteq2dv 
 |-  ( ( f = h /\ g = l ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
57 49 50 51 52 56 cbvmpo 
 |-  ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) ) = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
58 4 57 eqtri 
 |-  P = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
59 58 a1i 
 |-  ( ph -> P = ( h e. Y , l e. Y |-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) ) )
60 nfcv 
 |-  F/_ t 1
61 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )
62 3 3 61 nfmpo 
 |-  F/_ t ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
63 4 62 nfcxfr 
 |-  F/_ t P
64 nfcv 
 |-  F/_ t U
65 60 63 64 nfseq 
 |-  F/_ t seq 1 ( P , U )
66 nfcv 
 |-  F/_ t N
67 65 66 nffv 
 |-  F/_ t ( seq 1 ( P , U ) ` N )
68 67 nfeq2 
 |-  F/ t h = ( seq 1 ( P , U ) ` N )
69 nfv 
 |-  F/ t l = ( U ` ( N + 1 ) )
70 68 69 nfan 
 |-  F/ t ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) )
71 fveq1 
 |-  ( h = ( seq 1 ( P , U ) ` N ) -> ( h ` t ) = ( ( seq 1 ( P , U ) ` N ) ` t ) )
72 71 ad2antrr 
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( h ` t ) = ( ( seq 1 ( P , U ) ` N ) ` t ) )
73 fveq1 
 |-  ( l = ( U ` ( N + 1 ) ) -> ( l ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
74 73 ad2antlr 
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( l ` t ) = ( ( U ` ( N + 1 ) ) ` t ) )
75 72 74 oveq12d 
 |-  ( ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) /\ t e. T ) -> ( ( h ` t ) x. ( l ` t ) ) = ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
76 70 75 mpteq2da 
 |-  ( ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
77 76 adantl 
 |-  ( ( ph /\ ( h = ( seq 1 ( P , U ) ` N ) /\ l = ( U ` ( N + 1 ) ) ) ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
78 eqid 
 |-  ( seq 1 ( P , U ) ` N ) = ( seq 1 ( P , U ) ` N )
79 3simpc 
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( h e. Y /\ l e. Y ) )
80 nfcv 
 |-  F/_ f h
81 nfcv 
 |-  F/_ g h
82 nfcv 
 |-  F/_ g l
83 nfv 
 |-  F/ f h e. Y
84 nfv 
 |-  F/ f g e. Y
85 1 83 84 nf3an 
 |-  F/ f ( ph /\ h e. Y /\ g e. Y )
86 nfv 
 |-  F/ f ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y
87 85 86 nfim 
 |-  F/ f ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y )
88 nfv 
 |-  F/ g h e. Y
89 nfv 
 |-  F/ g l e. Y
90 2 88 89 nf3an 
 |-  F/ g ( ph /\ h e. Y /\ l e. Y )
91 nfv 
 |-  F/ g ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y
92 90 91 nfim 
 |-  F/ g ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
93 eleq1 
 |-  ( f = h -> ( f e. Y <-> h e. Y ) )
94 93 3anbi2d 
 |-  ( f = h -> ( ( ph /\ f e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ g e. Y ) ) )
95 53 oveq1d 
 |-  ( f = h -> ( ( f ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( g ` t ) ) )
96 95 mpteq2dv 
 |-  ( f = h -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) )
97 96 eleq1d 
 |-  ( f = h -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) )
98 94 97 imbi12d 
 |-  ( f = h -> ( ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y ) <-> ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) ) )
99 eleq1 
 |-  ( g = l -> ( g e. Y <-> l e. Y ) )
100 99 3anbi3d 
 |-  ( g = l -> ( ( ph /\ h e. Y /\ g e. Y ) <-> ( ph /\ h e. Y /\ l e. Y ) ) )
101 54 oveq2d 
 |-  ( g = l -> ( ( h ` t ) x. ( g ` t ) ) = ( ( h ` t ) x. ( l ` t ) ) )
102 101 mpteq2dv 
 |-  ( g = l -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) )
103 102 eleq1d 
 |-  ( g = l -> ( ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y <-> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
104 100 103 imbi12d 
 |-  ( g = l -> ( ( ( ph /\ h e. Y /\ g e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( g ` t ) ) ) e. Y ) <-> ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) ) )
105 80 81 82 87 92 98 104 8 vtocl2gf 
 |-  ( ( h e. Y /\ l e. Y ) -> ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y ) )
106 79 105 mpcom 
 |-  ( ( ph /\ h e. Y /\ l e. Y ) -> ( t e. T |-> ( ( h ` t ) x. ( l ` t ) ) ) e. Y )
107 58 78 9 7 106 6 fmulcl 
 |-  ( ph -> ( seq 1 ( P , U ) ` N ) e. Y )
108 mptexg 
 |-  ( T e. _V -> ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) e. _V )
109 6 108 syl 
 |-  ( ph -> ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) e. _V )
110 59 77 107 26 109 ovmpod 
 |-  ( ph -> ( ( seq 1 ( P , U ) ` N ) P ( U ` ( N + 1 ) ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
111 48 110 eqtrd 
 |-  ( ph -> ( seq 1 ( P , U ) ` ( N + 1 ) ) = ( t e. T |-> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) ) )
112 107 ancli 
 |-  ( ph -> ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) )
113 nfcv 
 |-  F/_ f 1
114 nfmpo1 
 |-  F/_ f ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
115 4 114 nfcxfr 
 |-  F/_ f P
116 nfcv 
 |-  F/_ f U
117 113 115 116 nfseq 
 |-  F/_ f seq 1 ( P , U )
118 nfcv 
 |-  F/_ f N
119 117 118 nffv 
 |-  F/_ f ( seq 1 ( P , U ) ` N )
120 119 nfel1 
 |-  F/ f ( seq 1 ( P , U ) ` N ) e. Y
121 1 120 nfan 
 |-  F/ f ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y )
122 nfcv 
 |-  F/_ f T
123 nfcv 
 |-  F/_ f RR
124 119 122 123 nff 
 |-  F/ f ( seq 1 ( P , U ) ` N ) : T --> RR
125 121 124 nfim 
 |-  F/ f ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR )
126 eleq1 
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( f e. Y <-> ( seq 1 ( P , U ) ` N ) e. Y ) )
127 126 anbi2d 
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( ( ph /\ f e. Y ) <-> ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) ) )
128 feq1 
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( f : T --> RR <-> ( seq 1 ( P , U ) ` N ) : T --> RR ) )
129 127 128 imbi12d 
 |-  ( f = ( seq 1 ( P , U ) ` N ) -> ( ( ( ph /\ f e. Y ) -> f : T --> RR ) <-> ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR ) ) )
130 119 125 129 12 vtoclgf 
 |-  ( ( seq 1 ( P , U ) ` N ) e. Y -> ( ( ph /\ ( seq 1 ( P , U ) ` N ) e. Y ) -> ( seq 1 ( P , U ) ` N ) : T --> RR ) )
131 107 112 130 sylc 
 |-  ( ph -> ( seq 1 ( P , U ) ` N ) : T --> RR )
132 131 ffvelcdmda 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` N ) ` t ) e. RR )
133 132 39 remulcld 
 |-  ( ( ph /\ t e. T ) -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) e. RR )
134 111 133 fvmpt2d 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
135 11 oveq1d 
 |-  ( ph -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
136 135 adantr 
 |-  ( ( ph /\ t e. T ) -> ( ( ( seq 1 ( P , U ) ` N ) ` t ) x. ( ( U ` ( N + 1 ) ) ` t ) ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
137 134 136 eqtrd 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( ( seq 1 ( x. , ( F ` t ) ) ` N ) x. ( ( U ` ( N + 1 ) ) ` t ) ) )
138 41 46 137 3eqtr4rd 
 |-  ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) )