let D be non empty set ; :: thesis: for f, CR being File of D ex r being File of D st r is_a_record_of f,CR
let f, CR be File of D; :: thesis: ex r being File of D st r is_a_record_of f,CR
set i0 = instr (1,(addcr (f,CR)),CR);
A1: instr (1,(addcr (f,CR)),CR) <> 0

proof

assume instr (1,(addcr (f,CR)),CR) = 0 ; :: thesis: contradiction
then not CR is_substring_of addcr (f,CR),1 by FINSEQ_8:def 10;
hence contradiction by Th40; :: thesis: verum

end;

then instr (1,(addcr (f,CR)),CR) > 0 ;
then A2: instr (1,(addcr (f,CR)),CR) >= 0 + 1 by NAT_1:13;
then (instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by XREAL_1:48;
then A3: (instr (1,(addcr (f,CR)),CR)) -' 1 = (instr (1,(addcr (f,CR)),CR)) - 1 by XREAL_0:def 2;

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

suppose len f = 0 ; :: thesis: ex r being File of D st r is_a_record_of f,CR

then f = <*> D ;
hence ex r being File of D st r is_a_record_of f,CR by Th22; :: thesis: verum

end;

suppose A4: len f <> 0 ; :: thesis: ex r being File of D st r is_a_record_of f,CR

set r = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1);
A5: CR is_preposition_of (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) by A1, FINSEQ_8:def 10;

now :: thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR

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

suppose A6: len CR <= 0 ; :: thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR

then A7: CR = <*> D ;
then CR /^ (len (ovlpart (f,CR))) = CR by FINSEQ_6:80;
then f ^ (CR /^ (len (ovlpart (f,CR)))) = f by A7, FINSEQ_1:34;
then A8: ovlcon (f,CR) = f by FINSEQ_8:def 3;
len f > 0 by A4;
then A9: len f >= 0 + 1 by NAT_1:13;
A10: ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) )

proof

assume len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 ; :: thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )
then A11: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= 0 + 1 by NAT_1:13;

per cases ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 or len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ) ;

suppose A12: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ; :: thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )

(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by FINSEQ_1:58
.= (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A12, FINSEQ_5:77
.= f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A8, FINSEQ_8:def 11
.= mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) by A11, FINSEQ_6:116 ;
hence ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) by A9; :: thesis: verum

end;

suppose A13: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 ; :: thesis: ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) )

A14: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by FINSEQ_5:17;
mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = f | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A11, FINSEQ_6:116
.= (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) by A8, FINSEQ_8:def 11 ;
hence ( 1 <= len f & mid (f,1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) by A9, A13, A14, XXREAL_0:1; :: thesis: verum

end;

end;

end;

A15: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by A6, FINSEQ_8:def 12;
addcr (f,CR) = f by A8, FINSEQ_8:def 11;
then (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_preposition_of addcr (f,CR) by A10, FINSEQ_8:def 8;
hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A15; :: thesis: verum

end;

suppose A16: len CR > 0 ; :: thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR

CR is_preposition_of (addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) by A1, FINSEQ_8:def 10;
then A17: len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by NAT_1:43;
then (instr (1,(addcr (f,CR)),CR)) -' 1 <= len (addcr (f,CR)) by A16, CARD_1:27, RFINSEQ:def 1;
then len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) = (len (addcr (f,CR))) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by RFINSEQ:def 1;
then A18: (len CR) + ((instr (1,(addcr (f,CR)),CR)) -' 1) <= len (addcr (f,CR)) by A17, XREAL_1:19;
A19: len CR >= 0 + 1 by A16, NAT_1:13;
mid (((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A5, A16, FINSEQ_8:def 8;
then ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR by A19, FINSEQ_6:116;
then A20: len CR <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by FINSEQ_5:16;
A21: len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len (addcr (f,CR)) by FINSEQ_5:25;

A22: now :: thesis: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR

per cases ( ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 >= len (addcr (f,CR)) or ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 < len (addcr (f,CR)) ) ;

suppose ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 >= len (addcr (f,CR)) ; :: thesis: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR

then (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = addcr (f,CR) by FINSEQ_1:58;
hence len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR by A20, A21, XXREAL_0:2; :: thesis: verum

end;

suppose A23: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 < len (addcr (f,CR)) ; :: thesis: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR

(instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by A2, XREAL_1:48;
then A24: (len CR) + ((instr (1,(addcr (f,CR)),CR)) - 1) >= (len CR) + 0 by XREAL_1:7;
then ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((len CR) + (instr (1,(addcr (f,CR)),CR))) - 1 by XREAL_0:def 2;
hence len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) >= len CR by A23, A24, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:48;
then A25: ((len CR) + (instr (1,(addcr (f,CR)),CR))) -' 1 <= len (addcr (f,CR)) by A3, A18, XREAL_0:def 2;
then A26: len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by FINSEQ_1:59;
( ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) ) & ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 ) )

proof

thus ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 implies ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) ) ) :: thesis: ( ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 implies not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 )

proof

assume ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) <> 0 ; :: thesis: ( 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) )
then 0 + 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) by NAT_1:13;
hence 1 <= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; :: thesis: ( CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) & ( for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ) )
set f2 = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1);
A27: instr (1,(addcr (f,CR)),CR) <= (instr (1,(addcr (f,CR)),CR)) + (len CR) by NAT_1:12;
(instr (1,(addcr (f,CR)),CR)) - 1 >= 0 by A2, XREAL_1:48;
then A28: (instr (1,(addcr (f,CR)),CR)) -' 1 = (instr (1,(addcr (f,CR)),CR)) - 1 by XREAL_0:def 2;
A29: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48;
then ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_0:def 2;
then (instr (1,(addcr (f,CR)),CR)) -' 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) by A3, A26, A27, XREAL_1:9;
then A30: len (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) = (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by RFINSEQ:def 1
.= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by A25, FINSEQ_1:59
.= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1) by A29, A28, XREAL_0:def 2
.= len CR ;
A31: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48;
(instr (1,(addcr (f,CR)),CR)) + (len CR) >= instr (1,(addcr (f,CR)),CR) by NAT_1:12;
then (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) >= 0 by NAT_D:42, XREAL_1:48;
then (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) -' ((instr (1,(addcr (f,CR)),CR)) -' 1) = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) - ((instr (1,(addcr (f,CR)),CR)) -' 1) by XREAL_0:def 2
.= (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) - ((instr (1,(addcr (f,CR)),CR)) - 1) by A3, A31, XREAL_0:def 2
.= len CR ;
then A32: ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) by FINSEQ_5:80;
mid (((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A5, A16, FINSEQ_8:def 8;
then ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) = CR by A19, A32, FINSEQ_6:116;
then (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) | (len CR) = CR by FINSEQ_1:58;
then A33: mid ((((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)),1,(len CR)) = CR by A19, FINSEQ_6:116;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48;
then A34: (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by XREAL_0:def 2
.= (instr (1,(addcr (f,CR)),CR)) + (len CR) ;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:48;
then (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by A26, XREAL_0:def 2;
then A35: ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = instr (1,(addcr (f,CR)),CR) by NAT_D:34;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 ;
then A36: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def 2;
(((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by A31, XREAL_0:def 2
.= (instr (1,(addcr (f,CR)),CR)) + (len CR) ;
then ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) = ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1) by A3, A18, A36, FINSEQ_1:59;
hence CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ ((((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)) -' 1) by A16, A30, A33, FINSEQ_8:def 8; :: thesis: for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 ;
then A37: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def 2;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48;
then A38: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 = ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_0:def 2;
thus for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) holds
j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) :: thesis: verum

proof

let j be Element of NAT ; :: thesis: ( j >= 1 & j > 0 & CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) implies j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) )
assume that
A39: j >= 1 and
j > 0 and
A40: CR is_preposition_of ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1) ; :: thesis: j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)
A41: (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR) = (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1)) by NAT_D:34
.= (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((len CR) + (j -' 1))) /^ (j -' 1) by FINSEQ_5:80 ;
A42: mid ((((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)),1,(len CR)) = (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) /^ (j -' 1)) | (len CR) by A19, FINSEQ_6:116;
A43: j - 1 >= 0 by A39, XREAL_1:48;

now :: thesis: not j < ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR)

assume A44: j < ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; :: thesis: contradiction
then j < instr (1,(addcr (f,CR)),CR) by A3, A18, A34, A37, FINSEQ_1:59;
then j -' 1 < (instr (1,(addcr (f,CR)),CR)) -' 1 by A39, NAT_D:56;
then A45: len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) <= len ((addcr (f,CR)) /^ (j -' 1)) by Th4;
A46: (j + (len CR)) - 1 >= 0 by A39, NAT_1:12, XREAL_1:48;
then A47: (j + (len CR)) -' 1 = (len CR) + (j - 1) by XREAL_0:def 2
.= (len CR) + (j -' 1) by A43, XREAL_0:def 2 ;
j < ((((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1) -' (len CR) by A25, A44, FINSEQ_1:59;
then j + (len CR) < (instr (1,(addcr (f,CR)),CR)) + (len CR) by A34, A37, XREAL_1:8;
then (j + (len CR)) - 1 < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 by XREAL_1:9;
then A48: (j + (len CR)) -' 1 < ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1 by A38, A46, XREAL_0:def 2;
((addcr (f,CR)) /^ (j -' 1)) | (len CR) = ((addcr (f,CR)) /^ (j -' 1)) | (((j -' 1) + (len CR)) -' (j -' 1)) by NAT_D:34
.= ((addcr (f,CR)) | ((len CR) + (j -' 1))) /^ (j -' 1) by FINSEQ_5:80
.= (((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) | ((j + (len CR)) -' 1)) /^ (j -' 1) by A47, A48, FINSEQ_5:77
.= CR by A16, A40, A42, A41, A47, FINSEQ_8:def 8 ;
then A49: mid (((addcr (f,CR)) /^ (j -' 1)),1,(len CR)) = CR by A19, FINSEQ_6:116;
1 <= len ((addcr (f,CR)) /^ ((instr (1,(addcr (f,CR)),CR)) -' 1)) by A5, A16, FINSEQ_8:def 8;
then 1 <= len ((addcr (f,CR)) /^ (j -' 1)) by A45, XXREAL_0:2;
then CR is_preposition_of (addcr (f,CR)) /^ (j -' 1) by A49, FINSEQ_8:def 8;
hence contradiction by A35, A39, A44, FINSEQ_8:def 10; :: thesis: verum

end;

hence j >= ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) ; :: thesis: verum

end;

end;

((instr (1,(addcr (f,CR)),CR)) + (len CR)) - (len CR) >= 0 ;
then A50: ((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' (len CR) = instr (1,(addcr (f,CR)),CR) by XREAL_0:def 2;
((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:48;
then A51: (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) + 1 = (((instr (1,(addcr (f,CR)),CR)) + (len CR)) - 1) + 1 by XREAL_0:def 2
.= (instr (1,(addcr (f,CR)),CR)) + (len CR) ;
assume ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) = 0 ; :: thesis: not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1
then instr (1,(addcr (f,CR)),CR) = 0 by A3, A18, A51, A50, FINSEQ_1:59;
then not CR is_substring_of addcr (f,CR),1 by FINSEQ_8:def 10;
hence not CR is_substring_of (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1),1 by A16, Th41; :: thesis: verum

end;

then A52: instr (1,((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)),CR) = ((len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1) -' (len CR) by FINSEQ_8:def 10;

per cases ( 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) or 1 > len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ) ;

suppose A53: 1 <= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ; :: thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR

( (addcr (f,CR)) | (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) & len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) <= len (addcr (f,CR)) ) by A25, FINSEQ_1:59;
then ( len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)))) = (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) ) ) by A53, FINSEQ_6:116, XXREAL_0:2;
then A54: ( CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (f,CR),1 or (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_preposition_of addcr (f,CR) ) by FINSEQ_8:def 8;
(addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by A22, A52, FINSEQ_8:def 12;
hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A54; :: thesis: verum

end;

suppose 1 > len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) ; :: thesis: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR

then A55: 0 + 1 >= (len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1))) + 1 by NAT_1:13;
then A56: len CR <= 0 by A22, XREAL_1:6;
then A57: (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_terminated_by CR by FINSEQ_8:def 12;
0 >= len ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) by A55, XREAL_1:6;
then (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) = {} ;
then CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) = CR by FINSEQ_1:34;
then CR ^ ((addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1)) is_substring_of addcr (f,CR),1 by A56, FINSEQ_8:def 7;
hence (addcr (f,CR)) | (((instr (1,(addcr (f,CR)),CR)) + (len CR)) -' 1) is_a_record_of f,CR by A57; :: thesis: verum

end;

end;

end;

end;

end;

hence ex r being File of D st r is_a_record_of f,CR ; :: thesis: verum

end;

end;