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

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

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

len CR >= 0 by NAT_1:2;
then 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 ^ CR is_preposition_of by A2, FINSEQ_8:def 8; :: thesis: verum

end;

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

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

end;

end;