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

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