let D be non empty set ; :: thesis: for f being FinSequence of D
for k2 being Nat st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
let f be FinSequence of D; :: thesis: for k2 being Nat st 1 <= k2 & k2 < len f holds
f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
let k2 be Nat; :: thesis: ( 1 <= k2 & k2 < len f implies f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) )
assume A1: ( 1 <= k2 & k2 < len f ) ; :: thesis: f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))
then mid (f,1,(len f)) = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) by INTEGRA2:4;
hence f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f))) by A1, FINSEQ_6:120, XXREAL_0:2; :: thesis: verum