let f1, f2 be XFinSequence; :: thesis: for n being Nat st n <= len f1 holds
(f1 ^ f2) /^ n = (f1 /^ n) ^ f2
let n be Nat; :: thesis: ( n <= len f1 implies (f1 ^ f2) /^ n = (f1 /^ n) ^ f2 )
assume n <= len f1 ; :: thesis: (f1 ^ f2) /^ n = (f1 /^ n) ^ f2
then A2: len (f1 | n) = n by AFINSQ_1:54;
f1 = (f1 | n) ^ (f1 /^ n) ;
then f1 ^ f2 = (f1 | n) ^ ((f1 /^ n) ^ f2) by AFINSQ_1:27;
hence (f1 ^ f2) /^ n = (f1 /^ n) ^ f2 by A2, AFINSQ_2:12; :: thesis: verum