let D be non empty set ; :: thesis: for f, CR being File of D holds f is_preposition_of f ^ CR
let f, CR be File of D; :: thesis: f is_preposition_of f ^ CR

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

suppose A1: len f > 0 ; :: thesis: f is_preposition_of f ^ CR

0 + 1 <= (len f) + (len CR) by A1, NAT_1:13;
then A2: 1 <= len (f ^ CR) by FINSEQ_1:22;
0 + 1 <= len f by A1, NAT_1:13;
then mid ((f ^ CR),1,(len f)) = f by FINSEQ_8:1;
hence f is_preposition_of f ^ CR by A2, FINSEQ_8:def 8; :: thesis: verum

end;

suppose len f <= 0 ; :: thesis: f is_preposition_of f ^ CR

hence f is_preposition_of f ^ CR by FINSEQ_8:def 8; :: thesis: verum

end;

end;