let f be non empty FinSequence; :: thesis: for g being FinSequence holds len g <= len (f ^' g)
let g be FinSequence; :: thesis: len g <= len (f ^' g)

per cases ( g = {} or g <> {} ) ;

suppose g = {} ; :: thesis: len g <= len (f ^' g)

hence len g <= len (f ^' g) ; :: thesis: verum

end;

suppose g <> {} ; :: thesis: len g <= len (f ^' g)

then A1: (len (f ^' g)) + 1 = (len f) + (len g) by GRAPH_2:13;
len f >= 1 by NAT_1:14;
then (len (f ^' g)) + 1 >= 1 + (len g) by A1, XREAL_1:8;
hence len g <= len (f ^' g) by XREAL_1:8; :: thesis: verum

end;

end;