let f be FinSequence; :: thesis: for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1
let l1, l2 be Nat; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

per cases ( l1 <= l2 or l1 > l2 ) ;

suppose A1: l1 <= l2 ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

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

suppose A2: l2 <= len f ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

then A3: l2 - l1 <= (len f) - l1 by XREAL_1:9;
A4: l1 <= len (f | l2) by A1, A2, FINSEQ_1:59;
then A5: len ((f | l2) /^ l1) = (len (f | l2)) - l1 by RFINSEQ:def 1
.= l2 - l1 by A2, FINSEQ_1:59
.= l2 -' l1 by A1, XREAL_1:233 ;
A6: l1 <= len f by A1, A2, XXREAL_0:2;
then len (f /^ l1) = (len f) - l1 by RFINSEQ:def 1;
then A7: l2 -' l1 <= len (f /^ l1) by A1, A3, XREAL_1:233;
A8: for k being Nat st 1 <= k & k <= len ((f | l2) /^ l1) holds
((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((f | l2) /^ l1) implies ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k )
assume that
A9: 1 <= k and
A10: k <= len ((f | l2) /^ l1) ; :: thesis: ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k
A11: k in dom ((f | l2) /^ l1) by A9, A10, FINSEQ_3:25;
k <= l2 - l1 by A1, A5, A10, XREAL_1:233;
then A12: k + l1 <= (l2 - l1) + l1 by XREAL_1:6;
k <= len (f /^ l1) by A7, A5, A10, XXREAL_0:2;
then A13: k in dom (f /^ l1) by A9, FINSEQ_3:25;
k in Seg (l2 -' l1) by A5, A9, A10;
then ((f /^ l1) | (l2 -' l1)) . k = (f /^ l1) . k by FUNCT_1:49
.= f . (k + l1) by A6, A13, RFINSEQ:def 1
.= (f | l2) . (k + l1) by A12, FINSEQ_3:112
.= ((f | l2) /^ l1) . k by A4, A11, RFINSEQ:def 1 ;
hence ((f /^ l1) | (l2 -' l1)) . k = ((f | l2) /^ l1) . k ; :: thesis: verum

end;

len ((f /^ l1) | (l2 -' l1)) = l2 -' l1 by A7, FINSEQ_1:59;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A5, A8; :: thesis: verum

end;

suppose A14: l2 > len f ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

A15: len (f /^ l1) = (len f) -' l1 by RFINSEQ:29;
f | l2 = f by A14, FINSEQ_1:58;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A14, A15, FINSEQ_1:58, NAT_D:42; :: thesis: verum

end;

end;

end;

suppose A16: l1 > l2 ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

reconsider l19 = l1, l29 = l2 as Element of NAT by ORDINAL1:def 12;
l1 - l1 > l2 - l1 by A16, XREAL_1:9;
then l2 -' l1 = 0 by XREAL_0:def 2;
then A17: (f /^ l1) | (l2 -' l1) = {} ;

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

suppose l1 <= len f ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

then l19 > len (f | l29) by A16, FINSEQ_1:59, XXREAL_0:2;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, Th32; :: thesis: verum

end;

suppose A18: l1 > len f ; :: thesis: (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1

len (f | l29) <= len f by Th16;
hence (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by A17, A18, Th32, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;