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 )
A2: len (r1 ^ r2) = (len r1) + (len r2) by FINSEQ_1:22;

A3: now :: thesis: r2 is_substring_of f,1

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

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

A5: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by XREAL_0:def 2
.= len r2 ;
A6: (len r1) + (len r2) > (len r1) + 0 by A4, XREAL_1:8;
len r2 >= 0 + 1 by A4, NAT_1:13;
then A7: (len r1) + 1 <= len (r1 ^ r2) by A2, XREAL_1:6;
then A8: 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 FINSEQ_6:def 3
.= (((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:22
.= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A6, NAT_2:7
.= ((r1 ^ (r2 ^ r3)) /^ (len r1)) | (len r2) by A5, FINSEQ_1:32
.= (r2 ^ r3) | (len r2)
.= r2 by FINSEQ_5:23 ;
A9: (len r1) + 1 >= 0 + 1 by XREAL_1:6;
A10: ((len r1) + 1) + 0 <= ((len r1) + (len r2)) + (len r3) by A2, A7, XREAL_1:7;
( 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

A11: (((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34
.= len (r1 ^ r2) by FINSEQ_1:22 ;
consider i being Element of NAT such that
A12: i = (len r1) + 1 ;
i <= len ((r1 ^ r2) ^ r3) by A2, A10, A12, FINSEQ_1:22;
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 ) ) by A9, A8, A12, A11; :: 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;

f = r1 ^ (r2 ^ r3) by A1, FINSEQ_1:32;
hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) by A1, A3, Th34; :: thesis: verum