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 Th41; :: thesis: verum

end;

then instr 1,(addcr f,CR),CR > 0 by NAT_1:3;
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:50;
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 r2 being File of D st r2 is_a_record_of f,CR by Th23; :: thesis: verum

end;

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

A5: ( 1 <= instr 1,(addcr f,CR),CR & (addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & (addcr f,CR) /^ (j -' 1) is_preposition_of holds
j >= instr 1,(addcr f,CR),CR ) ) by A1, FINSEQ_8:def 10;
set r = (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1);

now

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: len CR = 0 by NAT_1:2;
A8: (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_terminated_by CR by A6, FINSEQ_8:def 12;
A9: CR = <*> D by A7;
then CR /^ (len (ovlpart f,CR)) = CR by FINSEQ_6:86;
then f ^ (CR /^ (len (ovlpart f,CR))) = f by A9, FINSEQ_1:47;
then A10: ovlcon f,CR = f by FINSEQ_8:def 3;
then A11: addcr f,CR = f by FINSEQ_8:def 11;
len f > 0 by A4, NAT_1:3;
then A12: len f >= 0 + 1 by NAT_1:13;
( 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 A13: 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 A14: 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:79
.= (addcr f,CR) | (len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) by A14, FINSEQ_5:80
.= f | (len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) by A10, FINSEQ_8:def 11
.= mid f,1,(len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) by A13, JORDAN3:25 ;
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 A12; :: thesis: verum

end;

suppose A15: 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) )

A16: 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 A13, JORDAN3:25
.= (addcr f,CR) | (len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) by A10, FINSEQ_8:def 11 ;
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:19;
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 A12, A15, A16, XXREAL_0:1; :: thesis: verum

end;

end;

end;

then addcr f,CR is_preposition_of by A11, FINSEQ_8:def 8;
hence (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_a_record_of f,CR by A8, Def1; :: thesis: verum

end;

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

then A18: ( 1 <= len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) & mid ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)),1,(len CR) = CR ) by A5, FINSEQ_8:def 8;
A19: len CR >= 0 + 1 by A17, NAT_1:13;
then ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) | (len CR) = CR by A18, JORDAN3:25;
then A20: len CR <= len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) by FINSEQ_5:18;
A21: len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) <= len (addcr f,CR) by FINSEQ_5:28;

A22: now

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:79;
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:50;
then A24: (len CR) + ((instr 1,(addcr f,CR),CR) - 1) >= (len CR) + 0 by XREAL_1:9;
then ((instr 1,(addcr f,CR),CR) + (len CR)) -' 1 = ((len CR) + (instr 1,(addcr f,CR),CR)) - 1 by A17, 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:80; :: thesis: verum

end;

end;

end;

( 1 <= instr 1,(addcr f,CR),CR & (addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1) is_preposition_of ) by A1, FINSEQ_8:def 10;
then A25: len CR <= len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) by NAT_1:44;
then (instr 1,(addcr f,CR),CR) -' 1 <= len (addcr f,CR) by A17, CARD_1:47, RFINSEQ:def 2;
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 2;
then A26: (len CR) + ((instr 1,(addcr f,CR),CR) -' 1) <= len (addcr f,CR) by A25, XREAL_1:21;
((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:50;
then A27: ((len CR) + (instr 1,(addcr f,CR),CR)) -' 1 <= len (addcr f,CR) by A3, A26, XREAL_0:def 2;
then A28: 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:80;
( ( ((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) & ((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) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of 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) & ((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) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of 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) & ((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) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds
j >= ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR) ) )
then ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR) > 0 ;
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: ( ((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) is_preposition_of & ( for j being Element of NAT st j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of holds
j >= ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR) ) )
A29: ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:50;
then A30: (((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)) - (len CR) >= 0 by NAT_1:2;
then ((instr 1,(addcr f,CR),CR) + (len CR)) -' (len CR) = instr 1,(addcr f,CR),CR by XREAL_0:def 2;
then A31: ((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, A26, A30, FINSEQ_1:80;
(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:50;
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, A29, 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 JORDAN3:21;
set f2 = ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ ((instr 1,(addcr f,CR),CR) -' 1);
A33: ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:50;
then A34: ((instr 1,(addcr f,CR),CR) + (len CR)) -' 1 = ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 by XREAL_0:def 2;
instr 1,(addcr f,CR),CR <= (instr 1,(addcr f,CR),CR) + (len CR) by NAT_1:12;
then A35: (instr 1,(addcr f,CR),CR) -' 1 <= len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) by A3, A28, A34, XREAL_1:11;
(instr 1,(addcr f,CR),CR) - 1 >= 0 by A2, XREAL_1:50;
then A36: (instr 1,(addcr f,CR),CR) -' 1 = (instr 1,(addcr f,CR),CR) - 1 by XREAL_0:def 2;
A37: 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 A35, RFINSEQ:def 2
.= (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) - ((instr 1,(addcr f,CR),CR) -' 1) by A27, FINSEQ_1:80
.= (((instr 1,(addcr f,CR),CR) + (len CR)) - 1) - ((instr 1,(addcr f,CR),CR) - 1) by A33, A36, XREAL_0:def 2
.= len CR ;
mid ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)),1,(len CR) = CR by A5, A17, 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, JORDAN3:25;
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:79;
then ( 1 <= len (((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ ((instr 1,(addcr f,CR),CR) -' 1)) & 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, A37, JORDAN3:25;
hence ((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) is_preposition_of by A31, FINSEQ_8:def 8; :: thesis: for j being Element of NAT st j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of 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)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:50;
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 A28, XREAL_0:def 2;
then A38: ((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)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:50;
then A39: (((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)) - (len CR) >= 0 by NAT_1:2;
then A40: ((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:50;
then A41: ((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 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of 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 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of implies j >= ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR) )
assume A42: ( j >= 1 & j > 0 & ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) /^ (j -' 1) is_preposition_of ) ; :: thesis: j >= ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR)
A43: 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, JORDAN3:25;
A44: (((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 JORDAN3:21 ;
A45: j - 1 >= 0 by A42, XREAL_1:50;

now

assume A46: j < ((len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1) -' (len CR) ; :: thesis: contradiction
then A47: j < ((((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) + 1) -' (len CR) by A27, FINSEQ_1:80;
j < instr 1,(addcr f,CR),CR by A3, A26, A39, A40, A46, FINSEQ_1:80;
then A48: j -' 1 < (instr 1,(addcr f,CR),CR) -' 1 by A42, NAT_D:56;
A49: (j + (len CR)) - 1 >= 0 by A42, NAT_1:12, XREAL_1:50;
then A50: (j + (len CR)) -' 1 = (len CR) + (j - 1) by XREAL_0:def 2
.= (len CR) + (j -' 1) by A45, XREAL_0:def 2 ;
j + (len CR) < (instr 1,(addcr f,CR),CR) + (len CR) by A39, A40, A47, XREAL_1:10;
then (j + (len CR)) - 1 < ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 by XREAL_1:11;
then A51: (j + (len CR)) -' 1 < ((instr 1,(addcr f,CR),CR) + (len CR)) -' 1 by A41, A49, XREAL_0:def 2;
A52: ((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 JORDAN3:21
.= (((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) | ((j + (len CR)) -' 1)) /^ (j -' 1) by A50, A51, FINSEQ_5:80
.= CR by A17, A42, A43, A44, A50, FINSEQ_8:def 8 ;
A53: 1 <= len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) by A5, A17, FINSEQ_8:def 8;
len ((addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1)) <= len ((addcr f,CR) /^ (j -' 1)) by A48, Th4;
then ( 1 <= len ((addcr f,CR) /^ (j -' 1)) & mid ((addcr f,CR) /^ (j -' 1)),1,(len CR) = CR ) by A19, A52, A53, JORDAN3:25, XXREAL_0:2;
then (addcr f,CR) /^ (j -' 1) is_preposition_of by FINSEQ_8:def 8;
hence contradiction by A38, A42, A46, 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;

assume A54: ((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
((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= 0 by A19, NAT_1:12, XREAL_1:50;
then A55: (((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)) - (len CR) >= 0 by NAT_1:2;
then ((instr 1,(addcr f,CR),CR) + (len CR)) -' (len CR) = instr 1,(addcr f,CR),CR by XREAL_0:def 2;
then instr 1,(addcr f,CR),CR = 0 by A3, A26, A54, A55, FINSEQ_1:80;
then A56: not CR is_substring_of addcr f,CR,1 by FINSEQ_8:def 10;
(len CR) + (instr 1,(addcr f,CR),CR) >= (len CR) + 1 by A2, XREAL_1:9;
then ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= ((len CR) + 1) - 1 by XREAL_1:11;
then ((instr 1,(addcr f,CR),CR) + (len CR)) -' 1 >= len CR by XREAL_0:def 2;
hence not CR is_substring_of (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1),1 by A17, A56, Th42; :: thesis: verum

end;

then A58: ( len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) >= len CR & 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 A22, 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 A59: 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

A60: (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) by A27, FINSEQ_1:80;
len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) <= len (addcr f,CR) by FINSEQ_5:18;
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 A59, A60, JORDAN3:25, XXREAL_0:2;
then ( ( CR ^ ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) is_substring_of addcr f,CR,1 or addcr f,CR is_preposition_of ) & (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_terminated_by CR ) by A58, FINSEQ_8:def 8, FINSEQ_8:def 12;
hence (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_a_record_of f,CR by Def1; :: 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 A61: 0 + 1 >= (len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) + 1 by NAT_1:13;
then 0 >= len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) by XREAL_1:8;
then A62: 0 = len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) by NAT_1:2;
A63: len CR <= 0 by A22, A61, XREAL_1:8;
then A64: (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_terminated_by CR by FINSEQ_8:def 12;
(addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) = {} by A62;
then CR ^ ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) = CR by FINSEQ_1:47;
then CR ^ ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) is_substring_of addcr f,CR,1 by A63, FINSEQ_8:def 7;
hence (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) is_a_record_of f,CR by A64, Def1; :: 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;