let fin, fin1 be FinSequence; :: thesis: ( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) & ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) ) )
len (fin ^ fin1) = (len fin) + (len fin1) by FINSEQ_1:22;
hence ( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) ) by NAT_1:12; :: thesis: ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) )
assume fin <> {} ; :: thesis: ( 1 <= len fin & len fin1 < len (fin1 ^ fin) )
then A1: 0 + 1 <= len fin by NAT_1:13;
then (len fin1) + 1 <= (len fin) + (len fin1) by XREAL_1:6;
then (len fin1) + 1 <= len (fin1 ^ fin) by FINSEQ_1:22;
hence ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) by A1, NAT_1:13; :: thesis: verum