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 A1: g <> {} ; :: thesis: len g <= len (f ^' g)

A2: len f >= 1 by NAT_1:14;
(len (f ^' g)) + 1 = (len f) + (len g) by A1, FINSEQ_6:139;
then (len (f ^' g)) + 1 >= 1 + (len g) by A2, XREAL_1:6;
hence len g <= len (f ^' g) by XREAL_1:6; :: thesis: verum

end;

end;