let n be Nat; :: thesis: for K being Field
for f being FinSequence of NAT holds 1. (K,(f | n)) = (1. (K,f)) | n
let K be Field; :: thesis: for f being FinSequence of NAT holds 1. (K,(f | n)) = (1. (K,f)) | n
let f be FinSequence of NAT ; :: thesis: 1. (K,(f | n)) = (1. (K,f)) | n
dom (1. (K,(f | n))) = dom (f | n) by Def8;
then A1: len (1. (K,(f | n))) = len (f | n) by FINSEQ_3:29;
dom (1. (K,f)) = dom f by Def8;
then A2: len (1. (K,f)) = len f by FINSEQ_3:29;
per cases ( n > len f or n <= len f ) ;
suppose A3: n > len f ; :: thesis: 1. (K,(f | n)) = (1. (K,f)) | n
then f | n = f by FINSEQ_1:58;
hence 1. (K,(f | n)) = (1. (K,f)) | n by A2, A3, FINSEQ_1:58; :: thesis: verum
end;
suppose A4: n <= len f ; :: thesis: 1. (K,(f | n)) = (1. (K,f)) | n
f = (f | n) ^ (f /^ n) by RFINSEQ:8;
then A5: 1. (K,f) = (1. (K,(f | n))) ^ (1. (K,(f /^ n))) by Th58;
len (1. (K,(f | n))) = n by A1, A4, FINSEQ_1:59;
hence 1. (K,(f | n)) = (1. (K,f)) | n by A5, FINSEQ_5:23; :: thesis: verum
end;
end;