let k be Nat; :: thesis: for p, q being FinSequence st k > len p & k <= len (p ^ q) holds
ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q )
let p, q be FinSequence; :: thesis: ( k > len p & k <= len (p ^ q) implies ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q ) )
A1: 0 + 1 = 1 ;
assume that
A2: k > len p and
A3: k <= len (p ^ q) ; :: thesis: ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q )
consider l being Nat such that
A4: k = (len p) + l by A2, NAT_1:10;
take l ; :: thesis: ( k = (len p) + l & l >= 1 & l <= len q )
thus k = (len p) + l by A4; :: thesis: ( l >= 1 & l <= len q )
(len p) + l > (len p) + 0 by A2, A4;
then l > 0 ;
hence l >= 1 by A1, NAT_1:13; :: thesis: l <= len q
(len p) + l <= (len p) + (len q) by A3, A4, FINSEQ_1:22;
hence l <= len q by XREAL_1:6; :: thesis: verum