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

per cases ( n > len f or n <= len f ) ;

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

then ( f | n = f & (1. K,f) | n = 1. K,f ) by A1, FINSEQ_1:79;
hence 1. K,(f | n) = (1. K,f) | n ; :: thesis: verum

end;

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

then A2: len (1. K,(f | n)) = n by A1, FINSEQ_1:80;
f = (f | n) ^ (f /^ n) by RFINSEQ:21;
then 1. K,f = (1. K,(f | n)) ^ (1. K,(f /^ n)) by Th58;
hence 1. K,(f | n) = (1. K,f) | n by A2, FINSEQ_5:26; :: thesis: verum

end;

end;