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 r being File of D st r 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

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

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: CR = <*> D by NAT_1:2;
then CR /^ (len (ovlpart f,CR)) = CR by FINSEQ_6:86;
then f ^ (CR /^ (len (ovlpart f,CR))) = f by A7, FINSEQ_1:47;
then A8: ovlcon f,CR = f by FINSEQ_8:def 3;
len f > 0 by A4, NAT_1:3;
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:79
.= (addcr f,CR) | (len ((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1))) by A12, FINSEQ_5:80
.= 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, 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 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:19;
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, JORDAN3:25
.= (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 is_preposition_of 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, Def1; :: 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

(addcr f,CR) /^ ((instr 1,(addcr f,CR),CR) -' 1) is_preposition_of by A1, FINSEQ_8:def 10;
then A17: 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 A16, 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 A18: (len CR) + ((instr 1,(addcr f,CR),CR) -' 1) <= len (addcr f,CR) by A17, XREAL_1:21;
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, 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 A16, 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;

((instr 1,(addcr f,CR),CR) + (len CR)) - 1 >= 0 by A2, NAT_1:12, XREAL_1:50;
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: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 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) ) )
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:50;
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:50;
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:11;
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 2
.= (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) - ((instr 1,(addcr f,CR),CR) -' 1) by A25, FINSEQ_1:80
.= (((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:50;
(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, 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 JORDAN3:21;
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, 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 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, JORDAN3:25;
((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) + 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: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 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 by NAT_1:2;
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:80;
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 A16, A30, A33, 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)) - (len CR) >= 0 by NAT_1:2;
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:50;
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 & ((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 that
A39: j >= 1 and
j > 0 and
A40: ((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)
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 JORDAN3:21 ;
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, JORDAN3:25;
A43: j - 1 >= 0 by A39, XREAL_1:50;

now

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:80;
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:50;
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:80;
then j + (len CR) < (instr 1,(addcr f,CR),CR) + (len CR) by A34, A37, XREAL_1:10;
then (j + (len CR)) - 1 < ((instr 1,(addcr f,CR),CR) + (len CR)) - 1 by XREAL_1:11;
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 JORDAN3:21
.= (((addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1)) | ((j + (len CR)) -' 1)) /^ (j -' 1) by A47, A48, FINSEQ_5:80
.= 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, JORDAN3:25;
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 (addcr f,CR) /^ (j -' 1) is_preposition_of 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 by NAT_1:2;
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:50;
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:80;
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, Th42; :: 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:80, 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 A53, JORDAN3:25, 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 is_preposition_of ) 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, 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 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:8;
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:8;
then (addcr f,CR) | (((instr 1,(addcr f,CR),CR) + (len CR)) -' 1) = {} by NAT_1:2;
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 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, 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;