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 ) )
A1: len (r1 ^ r2) = (len r1) + (len r2) by FINSEQ_1:22;
assume A2: f = r1 ^ r2 ; :: thesis: ( r1 is_substring_of f,1 & r2 is_substring_of f,1 )
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
then A5: (len r1) + (len r2) > (len r1) + 0 by XREAL_1:8;
A6: r2 | (len r2) = r2 | (Seg (len r2)) by FINSEQ_1:def 16;
A7: ((len r1) + (len r2)) -' (len r1) = ((len r1) + (len r2)) - (len r1) by XREAL_0:def 2
.= len r2 ;
A8: len r2 >= 0 + 1 by A4, NAT_1:13;
then (len r1) + 1 <= len (r1 ^ r2) by A1, XREAL_1:6;
then A9: mid ((r1 ^ r2),((len r1) + 1),(len (r1 ^ r2))) = ((r1 ^ r2) /^ (((len r1) + 1) -' 1)) | (((len (r1 ^ r2)) -' ((len r1) + 1)) + 1) by FINSEQ_6:def 3
.= ((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:22
.= ((r1 ^ r2) /^ (len r1)) | (((len r1) + (len r2)) -' (len r1)) by A5, NAT_2:7
.= r2 | (len r2) by A7
.= r2 by A6, FINSEQ_2:20 ;
( 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
A10: i = (len r1) + 1 ;
A11: i <= len (r1 ^ r2) by A1, A8, A10, XREAL_1:6;
A12: (((len r1) + 1) -' 1) + (len r2) = (len r1) + (len r2) by NAT_D:34
.= len (r1 ^ r2) by FINSEQ_1:22 ;
1 <= i by A8, A10, XREAL_1:6;
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 ) ) by A9, A10, A12, A11; :: thesis: verum
end;
hence r2 is_substring_of f,1 by A2, FINSEQ_8:def 7; :: thesis: verum
end;
end;
end;
A13: ( len r2 >= 0 & len (r1 ^ r2) = (len r1) + (len r2) ) by FINSEQ_1:22;
now :: thesis: r1 is_substring_of f,1
per cases ( len r1 > 0 or len r1 <= 0 ) ;
suppose len r1 > 0 ; :: thesis: r1 is_substring_of f,1
then A14: len r1 >= 0 + 1 by NAT_1:13;
then A15: mid ((r1 ^ r2),1,(len r1)) = ((r1 ^ r2) /^ (1 -' 1)) | (((len r1) -' 1) + 1) by FINSEQ_6:def 3
.= ((r1 ^ r2) /^ 0) | (((len r1) -' 1) + 1) by XREAL_1:232
.= ((r1 ^ r2) /^ 0) | (len r1) by A14, XREAL_1:235
.= (r1 ^ r2) | (len r1)
.= r1 by FINSEQ_5:23 ;
( 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;
A16: (1 -' 1) + (len r1) = 0 + (len r1) by XREAL_1:232
.= len r1 ;
1 <= len (r1 ^ r2) by A13, A14, XREAL_1:7;
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 ) ) by A15, A16; :: thesis: verum
end;
hence r1 is_substring_of f,1 by A2, FINSEQ_8:def 7; :: thesis: verum
end;
end;
end;
hence ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) by A3; :: thesis: verum