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 g is_preposition_of f )
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:63;
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, FINSEQ_6:def 3
.= (f /^ (1 -' 1)) | (len g) by A3, XREAL_1:235
.= (f /^ 0) | (len g) by XREAL_1:232
.= f | (len g) by FINSEQ_5:28
.= g by A1, FINSEQ_3:113 ; :: thesis: verum
end;
assume A4: ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) ; :: thesis: g is_preposition_of f
per cases ( len g <= 0 or ( len g > 0 & mid (f,1,(len g)) = g ) ) by A4;
suppose len g <= 0 ; :: thesis: g is_preposition_of f
then g = {} ;
hence g is_preposition_of f by XBOOLE_1:2; :: thesis: verum
end;
suppose that A5: len g > 0 and
A6: mid (f,1,(len g)) = g ; :: thesis: g is_preposition_of f
0 + 1 <= len g by A5, NAT_1:13;
then g = f | (len g) by A6, FINSEQ_6:116;
hence g is_preposition_of f by RELAT_1:59; :: thesis: verum
end;
end;