let m, n be Nat; :: thesis: ( m <= n implies (primesFinS n) | m = primesFinS m )
set N = primesFinS n;
set M = primesFinS m;
assume A1: m <= n ; :: thesis: (primesFinS n) | m = primesFinS m
A2: len (primesFinS n) = n by Def1;
A3: len (primesFinS m) = m by Def1;
hence A4: len ((primesFinS n) | m) = len (primesFinS m) by A1, A2, FINSEQ_1:59; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((primesFinS n) | m) or ((primesFinS n) | m) . b₁ = (primesFinS m) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((primesFinS n) | m) or ((primesFinS n) | m) . k = (primesFinS m) . k )
assume that
A5: 1 <= k and
A6: k <= len ((primesFinS n) | m) ; :: thesis: ((primesFinS n) | m) . k = (primesFinS m) . k
reconsider z = k - 1 as Element of NAT by A5, INT_1:3;
A7: k in Seg m by A3, A4, A5, A6;
A8: z < m - 0 by A3, A4, A6, XREAL_1:8;
then A9: z < n by A1, XXREAL_0:2;
A10: k = z + 1 ;
thus ((primesFinS n) | m) . k = (primesFinS n) . k by A7, FUNCT_1:49
.= primenumber z by A9, A10, Def1
.= (primesFinS m) . k by A8, A10, Def1 ; :: thesis: verum