let D be non empty set ; :: thesis: for f being FinSequence of D
for k2 being Element of 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 Element of NAT st 1 <= k2 & k2 < len f holds
f = (mid f,1,k2) ^ (mid f,(k2 + 1),(len f))
let k2 be Element of 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, JORDAN3:29, XXREAL_0:2; :: thesis: verum