let D be non empty set ; :: thesis: for f1, f2 being FinSequence of D
for n being Nat st n <= len f1 holds
(f1 ^ f2) /^ n = (f1 /^ n) ^ f2

let f1, f2 be FinSequence of D; :: 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 A1: n <= len f1 ; :: thesis: (f1 ^ f2) /^ n = (f1 /^ n) ^ f2
reconsider n = n as Element of NAT by ORDINAL1:def 12;
len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
then len f1 <= len (f1 ^ f2) by NAT_1:11;
then A2: n <= len (f1 ^ f2) by ;
then A3: len ((f1 ^ f2) /^ n) = (len (f1 ^ f2)) - n by RFINSEQ:def 1;
A4: len ((f1 /^ n) ^ f2) = (len (f1 /^ n)) + (len f2) by FINSEQ_1:22
.= ((len f1) - n) + (len f2) by
.= ((len f1) + (len f2)) - n ;
A5: for i being Nat st 1 <= i & i <= len ((f1 ^ f2) /^ n) holds
((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len ((f1 ^ f2) /^ n) implies ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i )
assume that
A6: 1 <= i and
A7: i <= len ((f1 ^ f2) /^ n) ; :: thesis: ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i
i in Seg (len ((f1 ^ f2) /^ n)) by ;
then A8: i in dom ((f1 ^ f2) /^ n) by FINSEQ_1:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
now :: thesis: ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i
per cases ( i <= (len f1) - n or (len f1) - n < i ) ;
suppose A9: i <= (len f1) - n ; :: thesis: ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i
i <= i + n by NAT_1:11;
then A10: 1 <= i + n by ;
i + n <= len f1 by ;
then i + n in Seg (len f1) by ;
then A11: i + n in dom f1 by FINSEQ_1:def 3;
i <= len (f1 /^ n) by ;
then i in Seg (len (f1 /^ n)) by ;
then A12: i in dom (f1 /^ n) by FINSEQ_1:def 3;
then A13: ((f1 /^ n) ^ f2) . i = (f1 /^ n) . i by FINSEQ_1:def 7
.= f1 . (i + n) by ;
((f1 ^ f2) /^ n) . i = (f1 ^ f2) . (i + n) by
.= f1 . (i + n) by ;
hence ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i by A13; :: thesis: verum
end;
suppose A14: (len f1) - n < i ; :: thesis: ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i
then A15: len (f1 /^ n) < i by ;
i <= len ((f1 /^ n) ^ f2) by ;
then A16: ((f1 /^ n) ^ f2) . i = f2 . (i - (len (f1 /^ n))) by
.= f2 . (i - ((len f1) - n)) by
.= f2 . ((i + n) - (len f1)) ;
A17: i + n <= len (f1 ^ f2) by ;
A18: len f1 < i + n by ;
((f1 ^ f2) /^ n) . i = (f1 ^ f2) . (i + n) by
.= f2 . ((i + n) - (len f1)) by ;
hence ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i by A16; :: thesis: verum
end;
end;
end;
hence ((f1 ^ f2) /^ n) . i = ((f1 /^ n) ^ f2) . i ; :: thesis: verum
end;
len ((f1 ^ f2) /^ n) = len ((f1 /^ n) ^ f2) by ;
hence (f1 ^ f2) /^ n = (f1 /^ n) ^ f2 by ; :: thesis: verum