Step | Hyp | Ref
| Expression |
1 | | gsumval3.h |
. . . . . . 7
β’ (π β π»:(1...π)β1-1βπ΄) |
2 | | f1f 6784 |
. . . . . . 7
β’ (π»:(1...π)β1-1βπ΄ β π»:(1...π)βΆπ΄) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β π»:(1...π)βΆπ΄) |
4 | | fzfid 13934 |
. . . . . 6
β’ (π β (1...π) β Fin) |
5 | 3, 4 | fexd 7225 |
. . . . 5
β’ (π β π» β V) |
6 | | vex 3478 |
. . . . 5
β’ π β V |
7 | | coexg 7916 |
. . . . 5
β’ ((π» β V β§ π β V) β (π» β π) β V) |
8 | 5, 6, 7 | sylancl 586 |
. . . 4
β’ (π β (π» β π) β V) |
9 | 8 | ad2antrr 724 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π) β V) |
10 | | gsumval3.b |
. . . . 5
β’ π΅ = (BaseβπΊ) |
11 | | gsumval3.0 |
. . . . 5
β’ 0 =
(0gβπΊ) |
12 | | gsumval3.p |
. . . . 5
β’ + =
(+gβπΊ) |
13 | | gsumval3.z |
. . . . 5
β’ π = (CntzβπΊ) |
14 | | gsumval3.g |
. . . . 5
β’ (π β πΊ β Mnd) |
15 | | gsumval3.a |
. . . . 5
β’ (π β π΄ β π) |
16 | | gsumval3.f |
. . . . 5
β’ (π β πΉ:π΄βΆπ΅) |
17 | | gsumval3.c |
. . . . 5
β’ (π β ran πΉ β (πβran πΉ)) |
18 | | gsumval3.m |
. . . . 5
β’ (π β π β β) |
19 | | gsumval3.n |
. . . . 5
β’ (π β (πΉ supp 0 ) β ran π») |
20 | | gsumval3.w |
. . . . 5
β’ π = ((πΉ β π») supp 0 ) |
21 | 10, 11, 12, 13, 14, 15, 16, 17, 18, 1, 19, 20 | gsumval3lem1 19767 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) |
22 | | fzfi 13933 |
. . . . . . . 8
β’
(1...π) β
Fin |
23 | | suppssdm 8158 |
. . . . . . . . . 10
β’ ((πΉ β π») supp 0 ) β dom (πΉ β π») |
24 | 20, 23 | eqsstri 4015 |
. . . . . . . . 9
β’ π β dom (πΉ β π») |
25 | 16, 3 | fcod 6740 |
. . . . . . . . 9
β’ (π β (πΉ β π»):(1...π)βΆπ΅) |
26 | 24, 25 | fssdm 6734 |
. . . . . . . 8
β’ (π β π β (1...π)) |
27 | | ssfi 9169 |
. . . . . . . 8
β’
(((1...π) β Fin
β§ π β (1...π)) β π β Fin) |
28 | 22, 26, 27 | sylancr 587 |
. . . . . . 7
β’ (π β π β Fin) |
29 | 28 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β Fin) |
30 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π»:(1...π)β1-1βπ΄) |
31 | 26 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β (1...π)) |
32 | | f1ores 6844 |
. . . . . . . 8
β’ ((π»:(1...π)β1-1βπ΄ β§ π β (1...π)) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
33 | 30, 31, 32 | syl2anc 584 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
34 | 20 | imaeq2i 6055 |
. . . . . . . . . 10
β’ (π» β π) = (π» β ((πΉ β π») supp 0 )) |
35 | 16, 15 | fexd 7225 |
. . . . . . . . . . . . 13
β’ (π β πΉ β V) |
36 | | ovex 7438 |
. . . . . . . . . . . . . 14
β’
(1...π) β
V |
37 | | fex 7224 |
. . . . . . . . . . . . . 14
β’ ((π»:(1...π)βΆπ΄ β§ (1...π) β V) β π» β V) |
38 | 3, 36, 37 | sylancl 586 |
. . . . . . . . . . . . 13
β’ (π β π» β V) |
39 | 35, 38 | jca 512 |
. . . . . . . . . . . 12
β’ (π β (πΉ β V β§ π» β V)) |
40 | | f1fun 6786 |
. . . . . . . . . . . . . 14
β’ (π»:(1...π)β1-1βπ΄ β Fun π») |
41 | 1, 40 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β Fun π») |
42 | 41, 19 | jca 512 |
. . . . . . . . . . . 12
β’ (π β (Fun π» β§ (πΉ supp 0 ) β ran π»)) |
43 | | imacosupp 8190 |
. . . . . . . . . . . 12
β’ ((πΉ β V β§ π» β V) β ((Fun π» β§ (πΉ supp 0 ) β ran π») β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 ))) |
44 | 39, 42, 43 | sylc 65 |
. . . . . . . . . . 11
β’ (π β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 )) |
45 | 44 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 )) |
46 | 34, 45 | eqtrid 2784 |
. . . . . . . . 9
β’ ((π β§ π β β
) β (π» β π) = (πΉ supp 0 )) |
47 | 46 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π) = (πΉ supp 0 )) |
48 | 47 | f1oeq3d 6827 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» βΎ π):πβ1-1-ontoβ(π» β π) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 ))) |
49 | 33, 48 | mpbid 231 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 )) |
50 | 29, 49 | hasheqf1od 14309 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β
(β―βπ) =
(β―β(πΉ supp
0
))) |
51 | 50 | fveq2d 6892 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β (π» β π)))β(β―β(πΉ supp 0 )))) |
52 | 21, 51 | jca 512 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β (π» β π)))β(β―β(πΉ supp 0 ))))) |
53 | | f1oeq1 6818 |
. . . 4
β’ (π = (π» β π) β (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) |
54 | | coeq2 5856 |
. . . . . . 7
β’ (π = (π» β π) β (πΉ β π) = (πΉ β (π» β π))) |
55 | 54 | seqeq3d 13970 |
. . . . . 6
β’ (π = (π» β π) β seq1( + , (πΉ β π)) = seq1( + , (πΉ β (π» β π)))) |
56 | 55 | fveq1d 6890 |
. . . . 5
β’ (π = (π» β π) β (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))) = (seq1( + , (πΉ β (π» β π)))β(β―β(πΉ supp 0 )))) |
57 | 56 | eqeq2d 2743 |
. . . 4
β’ (π = (π» β π) β ((seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))) β (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β (π» β π)))β(β―β(πΉ supp 0 ))))) |
58 | 53, 57 | anbi12d 631 |
. . 3
β’ (π = (π» β π) β ((π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β ((π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β (π» β π)))β(β―β(πΉ supp 0 )))))) |
59 | 9, 52, 58 | spcedv 3588 |
. 2
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) |
60 | 14 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β πΊ β Mnd) |
61 | 15 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π΄ β π) |
62 | 16 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β πΉ:π΄βΆπ΅) |
63 | 17 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ran πΉ β (πβran πΉ)) |
64 | | f1f1orn 6841 |
. . . . . . . . . . . . 13
β’ (π»:(1...π)β1-1βπ΄ β π»:(1...π)β1-1-ontoβran
π») |
65 | 1, 64 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π»:(1...π)β1-1-ontoβran
π») |
66 | | f1oen3g 8958 |
. . . . . . . . . . . 12
β’ ((π» β V β§ π»:(1...π)β1-1-ontoβran
π») β (1...π) β ran π») |
67 | 5, 65, 66 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (1...π) β ran π») |
68 | | enfi 9186 |
. . . . . . . . . . 11
β’
((1...π) β ran
π» β ((1...π) β Fin β ran π» β Fin)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
β’ (π β ((1...π) β Fin β ran π» β Fin)) |
70 | 22, 69 | mpbii 232 |
. . . . . . . . 9
β’ (π β ran π» β Fin) |
71 | 70, 19 | ssfid 9263 |
. . . . . . . 8
β’ (π β (πΉ supp 0 ) β
Fin) |
72 | 71 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΉ supp 0 ) β
Fin) |
73 | 20 | neeq1i 3005 |
. . . . . . . . . 10
β’ (π β β
β ((πΉ β π») supp 0 ) β
β
) |
74 | | supp0cosupp0 8189 |
. . . . . . . . . . . 12
β’ ((πΉ β V β§ π» β V) β ((πΉ supp 0 ) = β
β ((πΉ β π») supp 0 ) =
β
)) |
75 | 74 | necon3d 2961 |
. . . . . . . . . . 11
β’ ((πΉ β V β§ π» β V) β (((πΉ β π») supp 0 ) β β
β
(πΉ supp 0 ) β
β
)) |
76 | 35, 38, 75 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (((πΉ β π») supp 0 ) β β
β
(πΉ supp 0 ) β
β
)) |
77 | 73, 76 | biimtrid 241 |
. . . . . . . . 9
β’ (π β (π β β
β (πΉ supp 0 ) β
β
)) |
78 | 77 | imp 407 |
. . . . . . . 8
β’ ((π β§ π β β
) β (πΉ supp 0 ) β
β
) |
79 | 78 | adantr 481 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΉ supp 0 ) β
β
) |
80 | 19 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΉ supp 0 ) β ran π») |
81 | 3 | frnd 6722 |
. . . . . . . . 9
β’ (π β ran π» β π΄) |
82 | 81 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ran π» β π΄) |
83 | 80, 82 | sstrd 3991 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΉ supp 0 ) β π΄) |
84 | 10, 11, 12, 13, 60, 61, 62, 63, 72, 79, 83 | gsumval3eu 19766 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β β!π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) |
85 | | iota1 6517 |
. . . . . 6
β’
(β!π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (β©π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) = π₯)) |
86 | 84, 85 | syl 17 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (β©π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) = π₯)) |
87 | | eqid 2732 |
. . . . . . 7
β’ (πΉ supp 0 ) = (πΉ supp 0 ) |
88 | | simprl 769 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β Β¬ π΄ β ran
...) |
89 | 10, 11, 12, 13, 60, 61, 62, 63, 72, 79, 87, 88 | gsumval3a 19765 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΊ Ξ£g
πΉ) = (β©π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))))) |
90 | 89 | eqeq1d 2734 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((πΊ Ξ£g
πΉ) = π₯ β (β©π₯βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) = π₯)) |
91 | 86, 90 | bitr4d 281 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = π₯)) |
92 | 91 | alrimiv 1930 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β βπ₯(βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = π₯)) |
93 | | fvex 6901 |
. . . 4
β’ (seq1(
+ ,
(πΉ β (π» β π)))β(β―βπ)) β V |
94 | | eqeq1 2736 |
. . . . . . 7
β’ (π₯ = (seq1( + , (πΉ β (π» β π)))β(β―βπ)) β (π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))) β (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 ))))) |
95 | 94 | anbi2d 629 |
. . . . . 6
β’ (π₯ = (seq1( + , (πΉ β (π» β π)))β(β―βπ)) β ((π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))))) |
96 | 95 | exbidv 1924 |
. . . . 5
β’ (π₯ = (seq1( + , (πΉ β (π» β π)))β(β―βπ)) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))))) |
97 | | eqeq2 2744 |
. . . . 5
β’ (π₯ = (seq1( + , (πΉ β (π» β π)))β(β―βπ)) β ((πΊ Ξ£g πΉ) = π₯ β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ)))) |
98 | 96, 97 | bibi12d 345 |
. . . 4
β’ (π₯ = (seq1( + , (πΉ β (π» β π)))β(β―βπ)) β ((βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = π₯) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ))))) |
99 | 93, 98 | spcv 3595 |
. . 3
β’
(βπ₯(βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ π₯ = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = π₯) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ)))) |
100 | 92, 99 | syl 17 |
. 2
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (βπ(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β§ (seq1( + , (πΉ β (π» β π)))β(β―βπ)) = (seq1( + , (πΉ β π))β(β―β(πΉ supp 0 )))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ)))) |
101 | 59, 100 | mpbid 231 |
1
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ))) |