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

A6: now

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

suppose len r1 > 0 ; :: thesis: r1 is_substring_of f,1

then A7: len r1 >= 0 + 1 by NAT_1:13;
then A8: mid (r1 ^ r2),1,(len r1) = ((r1 ^ r2) /^ (1 -' 1)) | (((len r1) -' 1) + 1) by JORDAN3:def 1
.= ((r1 ^ r2) /^ 0 ) | (((len r1) -' 1) + 1) by XREAL_1:234
.= ((r1 ^ r2) /^ 0 ) | (len r1) by A7, XREAL_1:237
.= (r1 ^ r2) | (len r1) by FINSEQ_5:31
.= r1 by FINSEQ_5:26 ;
( len r1 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len (r1 ^ r2) & mid (r1 ^ r2),i,((i -' 1) + (len r1)) = r1 ) )

proof

set i = 1;
(1 -' 1) + (len r1) = 0 + (len r1) by XREAL_1:234
.= len r1 ;
then ( 1 <= 1 & 1 <= len (r1 ^ r2) & mid (r1 ^ r2),1,((1 -' 1) + (len r1)) = r1 ) by A3, A5, A7, A8, XREAL_1:9;
hence ( len r1 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len (r1 ^ r2) & mid (r1 ^ r2),i,((i -' 1) + (len r1)) = r1 ) ) ; :: thesis: verum

end;

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

end;

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

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

end;

end;

end;

now

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

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

then A10: len r2 >= 0 + 1 by NAT_1:13;
then A11: (len r1) + 1 <= len (r1 ^ r2) by A4, XREAL_1:8;
A12: (len r1) + (len r2) > (len r1) + 0 by A9, XREAL_1:10;
A13: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by A9, XREAL_0:def 2
.= len r2 ;
A14: r2 | (len r2) = r2 | (Seg (len r2)) by FINSEQ_1:def 15;
A15: mid (r1 ^ r2),((len r1) + 1),(len (r1 ^ r2)) = ((r1 ^ r2) /^ (((len r1) + 1) -' 1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by A11, JORDAN3:def 1
.= ((r1 ^ r2) /^ (len r1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by NAT_D:34
.= ((r1 ^ r2) /^ (len r1)) | ((((len r1) + (len r2)) -' ((len r1) + 1)) + 1) by FINSEQ_1:35
.= ((r1 ^ r2) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A12, NAT_2:9
.= r2 | (len r2) by A13, FINSEQ_5:40
.= r2 by A14, FINSEQ_2:23 ;
( len r2 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len (r1 ^ r2) & mid (r1 ^ r2),i,((i -' 1) + (len r2)) = r2 ) )

proof

consider i being Element of NAT such that
A16: 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) & mid (r1 ^ r2),i,((i -' 1) + (len r2)) = r2 ) by A4, A10, A15, A16, XREAL_1:8;
hence ( len r2 > 0 implies ex i being Element of NAT st
( 1 <= i & i <= len (r1 ^ r2) & mid (r1 ^ r2),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 ) by A6; :: thesis: verum