let D be non empty set ; :: thesis: for a, b being set
for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let a, b be set ; :: thesis: for f, r, CR being File of D st a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let f, r, CR be File of D; :: thesis: ( a <> b & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> implies ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) )
assume that
A1: a <> b and
A2: CR = <*b*> and
A3: f = <*b,a,b*> and
A4: r = <*a,b*> ; :: thesis: ( CR is_a_record_of f,CR & r is_a_record_of f,CR )
reconsider b2 = b, a2 = a as Element of D by A3, Th10;
A5: ( CR . 1 = b & len CR = 1 ) by A2, FINSEQ_1:40;
f = <*b,a*> ^ <*b*> by A3, FINSEQ_1:43
.= (f | 2) ^ CR by A2, A3, Th14 ;
then ovlpart (f,CR) = CR by FINSEQ_8:14;
then CR /^ (len (ovlpart (f,CR))) = {} by FINSEQ_6:167;
then f ^ (CR /^ (len (ovlpart (f,CR)))) = f by FINSEQ_1:34;
then A6: ovlcon (f,CR) = f by FINSEQ_8:def 3;
A7: f = CR ^ r by A2, A3, A4, FINSEQ_1:43;
then A8: len f = (len CR) + (len r) by FINSEQ_1:22
.= 1 + (len <*a,b*>) by A2, A4, FINSEQ_1:40
.= 1 + 2 by FINSEQ_1:44
.= 3 ;
then CR ^ r is_substring_of f,1 by A7, FINSEQ_8:19;
then A9: CR ^ r is_substring_of addcr (f,CR),1 by A6, FINSEQ_8:def 11;
A10: len CR = 1 by A2, FINSEQ_1:40;
then mid (f,1,(len CR)) = (f /^ (1 -' 1)) | ((1 -' 1) + 1) by FINSEQ_6:def 3
.= (f /^ (1 -' 1)) | (1 + 0) by NAT_2:8
.= (f /^ 0) | 1 by NAT_D:34
.= f | 1
.= <*b2,a2,b2*> | (Seg 1) by A3, FINSEQ_1:def 16
.= CR by A2, FINSEQ_6:4 ;
then CR is_preposition_of f by A8, FINSEQ_8:def 8;
then A11: CR is_preposition_of addcr (f,CR) by A6, FINSEQ_8:def 11;
r /^ (1 -' 1) = r /^ ((0 + 1) -' 1)
.= r /^ 0 by NAT_D:34
.= r ;
then (r /^ (1 -' 1)) . 1 = a by A4;
then A12: not CR is_preposition_of r /^ (1 -' 1) by A1, A5, FINSEQ_8:21;
A13: for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of r /^ (j -' 1) holds
j >= 2

proof

let j be Element of NAT ; :: thesis: ( j >= 1 & j > 0 & CR is_preposition_of r /^ (j -' 1) implies j >= 2 )
assume that
A14: j >= 1 and
j > 0 and
A15: CR is_preposition_of r /^ (j -' 1) ; :: thesis: j >= 2
j > 1 by A12, A14, A15, XXREAL_0:1;
then 1 + 1 <= j by NAT_1:13;
hence j >= 2 ; :: thesis: verum

end;

r /^ (2 -' 1) = r /^ ((1 + 1) -' 1)
.= <*a2,b2*> /^ 1 by A4, NAT_D:34
.= CR by A2, FINSEQ_6:46 ;
then A16: instr (1,r,CR) = 2 by A13, FINSEQ_8:def 10;
A17: len r = 2 by A4, FINSEQ_1:44;
then ((len r) + 1) -' (len CR) = 2 by A10, NAT_D:34;
then ( CR is_terminated_by CR & r is_terminated_by CR ) by A10, A17, A16, FINSEQ_8:28, FINSEQ_8:def 12;
hence ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) by A11, A9; :: thesis: verum