let D be non empty set ; for f, g being FinSequence of D st len f >= 1 holds
mid (f ^ g),1,(len f) = f
let f, g be FinSequence of D; ( len f >= 1 implies mid (f ^ g),1,(len f) = f )
assume A1:
len f >= 1
; mid (f ^ g),1,(len f) = f
then
(len f) - 1 >= 0
by XREAL_1:50;
then
(len f) - 1 = (len f) -' 1
by XREAL_0:def 2;
then A2:
((len f) -' 1) + 1 = len f
;
1 - 1 = 0
;
then A3:
1 -' 1 = 0
by XREAL_0:def 2;
(f ^ g) | (len f) = f
by FINSEQ_5:26;
then
((f ^ g) /^ 0 ) | (len f) = f
by FINSEQ_5:31;
hence
mid (f ^ g),1,(len f) = f
by A1, A2, A3, JORDAN3:def 1; verum