let f be FinSequence; :: thesis: for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
let i1, i2 be Nat; :: thesis: ( i1 <= i2 implies ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 ) )
assume A1: i1 <= i2 ; :: thesis: ( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )
len (f | i1) <= i1 by Th17;
hence (f | i1) | i2 = f | i1 by A1, FINSEQ_1:58, XXREAL_0:2; :: thesis: (f | i2) | i1 = f | i1
Seg i1 c= Seg i2 by A1, FINSEQ_1:5;
hence (f | i2) | i1 = f | i1 by FUNCT_1:51; :: thesis: verum