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:31;
dom (1. K,f) = dom f by Def8;
then A2: len (1. K,f) = len f by FINSEQ_3:31;

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:79;
hence 1. K,(f | n) = (1. K,f) | n by A2, A3, FINSEQ_1:79; :: thesis: verum

end;

suppose A4: n <= len f ; :: thesis: 1. K,(f | n) = (1. K,f) | n

f = (f | n) ^ (f /^ n) by RFINSEQ:21;
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:80;
hence 1. K,(f | n) = (1. K,f) | n by A5, FINSEQ_5:26; :: thesis: verum

end;

end;