thus ( g c= f & len g > 0 implies ( 1 <= len f & mid f,1,(len g) = g ) ) :: thesis: ( ( len g > 0 implies ( 1 <= len f & mid f,1,(len g) = g ) ) implies f is_preposition_of )

proof

assume that
A1: g c= f and
A2: len g > 0 ; :: thesis: ( 1 <= len f & mid f,1,(len g) = g )
A3: 0 + 1 <= len g by A2, NAT_1:13;
len g <= len f by A1, FINSEQ_1:84;
hence 1 <= len f by A3, XXREAL_0:2; :: thesis: mid f,1,(len g) = g
thus mid f,1,(len g) = (f /^ (1 -' 1)) | (((len g) -' 1) + 1) by A3, JORDAN3:def 1
.= (f /^ (1 -' 1)) | (len g) by A3, XREAL_1:237
.= (f /^ 0 ) | (len g) by XREAL_1:234
.= f | (len g) by FINSEQ_5:31
.= g by A1, FINSEQ_3:122 ; :: thesis: verum

end;

assume A4: ( len g > 0 implies ( 1 <= len f & mid f,1,(len g) = g ) ) ; :: thesis: f is_preposition_of

per cases ( len g <= 0 or ( len g > 0 & mid f,1,(len g) = g ) ) by A4;

suppose len g <= 0 ; :: thesis: f is_preposition_of

then len g = 0 ;
then g = {} ;
hence f is_preposition_of by XBOOLE_1:2; :: thesis: verum

end;

suppose that A5: len g > 0 and
A6: mid f,1,(len g) = g ; :: thesis: f is_preposition_of

0 + 1 <= len g by A5, NAT_1:13;
then g = f | (len g) by A6, JORDAN3:25;
hence f is_preposition_of by RELAT_1:88; :: thesis: verum

end;

end;