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 A1, XXREAL_0:2;
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 A1, RFINSEQ:def 1
.= ((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 A6, A7, FINSEQ_1:1;
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 A6, XXREAL_0:2;
i + n <= len f1 by A9, XREAL_1:19;
then i + n in Seg (len f1) by A10, FINSEQ_1:1;
then A11: i + n in dom f1 by FINSEQ_1:def 3;
i <= len (f1 /^ n) by A1, A9, RFINSEQ:def 1;
then i in Seg (len (f1 /^ n)) by A6, FINSEQ_1:1;
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 A1, A12, RFINSEQ:def 1 ;
((f1 ^ f2) /^ n) . i = (f1 ^ f2) . (i + n) by A2, A8, RFINSEQ:def 1
.= f1 . (i + n) by A11, FINSEQ_1:def 7 ;
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 A1, RFINSEQ:def 1;
i <= len ((f1 /^ n) ^ f2) by A3, A4, A7, FINSEQ_1:22;
then A16: ((f1 /^ n) ^ f2) . i = f2 . (i - (len (f1 /^ n))) by A15, FINSEQ_1:24
.= f2 . (i - ((len f1) - n)) by A1, RFINSEQ:def 1
.= f2 . ((i + n) - (len f1)) ;
A17: i + n <= len (f1 ^ f2) by A3, A7, XREAL_1:19;
A18: len f1 < i + n by A14, XREAL_1:19;
((f1 ^ f2) /^ n) . i = (f1 ^ f2) . (i + n) by A2, A8, RFINSEQ:def 1
.= f2 . ((i + n) - (len f1)) by A18, A17, FINSEQ_1:24 ;
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 A3, A4, FINSEQ_1:22;
hence (f1 ^ f2) /^ n = (f1 /^ n) ^ f2 by A5, FINSEQ_1:14; :: thesis: verum