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:35;
A3: len r3 >= 0 by NAT_1:2;

A4: now

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

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

then A6: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by XREAL_0:def 2
.= len r2 ;
A7: (len r1) + (len r2) > (len r1) + 0 by A5, XREAL_1:10;
len r2 >= 0 + 1 by A5, NAT_1:13;
then A8: (len r1) + 1 <= len (r1 ^ r2) by A2, XREAL_1:8;
then A9: 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:35
.= (((r1 ^ r2) ^ r3) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A7, NAT_2:9
.= ((r1 ^ (r2 ^ r3)) /^ (len r1)) | (len r2) by A6, FINSEQ_1:45
.= (r2 ^ r3) | (len r2) by FINSEQ_5:40
.= r2 by FINSEQ_5:26 ;
len r1 >= 0 by NAT_1:2;
then A10: (len r1) + 1 >= 0 + 1 by XREAL_1:8;
A11: ((len r1) + 1) + 0 <= ((len r1) + (len r2)) + (len r3) by A3, A2, A8, XREAL_1:9;
( 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

A12: (((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34
.= len (r1 ^ r2) by FINSEQ_1:35 ;
consider i being Element of NAT such that
A13: i = (len r1) + 1 ;
i <= len ((r1 ^ r2) ^ r3) by A2, A11, A13, 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 ) ) by A10, A9, A13, A12; :: 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:45;
hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3 is_substring_of f,1 ) by A1, A4, Th35; :: thesis: verum