let D be non empty set ; :: thesis: for r1, r2, r3, f being File of D st f = (r1 ^ r2) ^ r3 holds
( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 )
let r1, r2, r3, f be File of D; :: thesis: ( f = (r1 ^ r2) ^ r3 implies ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) )
assume A1: f = (r1 ^ r2) ^ r3 ; :: thesis: ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 )
then A2: f = r1 ^ (r2 ^ r3) by FINSEQ_1:45;
A3: len r3 >= 0 by NAT_1:2;
A4: len (r1 ^ r2) = (len r1) + (len r2) by FINSEQ_1:35;

now

per cases ( len r2 > 0 or len r2 <= 0 ) ;

suppose A5: len r2 > 0 ; :: thesis: r2 is_substring_of f,1

then len r2 >= 0 + 1 by NAT_1:13;
then A6: (len r1) + 1 <= len (r1 ^ r2) by A4, XREAL_1:8;
then A7: ((len r1) + 1) + 0 <= ((len r1) + (len r2)) + (len r3) by A3, A4, XREAL_1:9;
len r1 >= 0 by NAT_1:2;
then A8: (len r1) + 1 >= 0 + 1 by XREAL_1:8;
A9: (len r1) + (len r2) > (len r1) + 0 by A5, XREAL_1:10;
A10: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by A5, XREAL_0:def 2
.= len r2 ;
A11: mid ((r1 ^ r2) ^ r3),((len r1) + 1),(len (r1 ^ r2)) = (((r1 ^ r2) ^ r3) /^ (((len r1) + 1) -' 1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by A6, JORDAN3:def 1
.= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by NAT_D:34
.= (((r1 ^ r2) ^ r3) /^ (len r1)) | ((((len r1) + (len r2)) -' ((len r1) + 1)) + 1) by FINSEQ_1:35
.= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A9, NAT_2:9
.= ((r1 ^ (r2 ^ r3)) /^ (len r1)) | (len r2) by A10, FINSEQ_1:45
.= (r2 ^ r3) | (len r2) by FINSEQ_5:40
.= r2 by FINSEQ_5:26 ;
( len r2 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len ((r1 ^ r2) ^ r3) & mid ((r1 ^ r2) ^ r3),i,((i -' 1) + (len r2)) = r2 ) )

proof

consider i being Element of NAT such that
A12: i = (len r1) + 1 ;
(((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34
.= len (r1 ^ r2) by FINSEQ_1:35 ;
then ( 1 <= i & i <= len ((r1 ^ r2) ^ r3) & mid ((r1 ^ r2) ^ r3),i,((i -' 1) + (len r2)) = r2 ) by A4, A7, A8, A11, A12, FINSEQ_1:35;
hence ( len r2 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len ((r1 ^ r2) ^ r3) & mid ((r1 ^ r2) ^ r3),i,((i -' 1) + (len r2)) = r2 ) ) ; :: thesis: verum

end;

hence r2 is_substring_of f,1 by A1, FINSEQ_8:def 7; :: thesis: verum

end;

suppose len r2 <= 0 ; :: thesis: r2 is_substring_of f,1

hence r2 is_substring_of f,1 by FINSEQ_8:def 7; :: thesis: verum

end;

end;

end;

hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) by A1, A2, Th35; :: thesis: verum