let E be non empty set ; :: thesis: for u, v, w being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds
( len u < len w & len v < len w )
let u, v, w be Element of E ^omega ; :: thesis: ( w = u ^ v & u <> <%> E & v <> <%> E implies ( len u < len w & len v < len w ) )
assume that
A1: w = u ^ v and
A2: u <> <%> E and
A3: v <> <%> E ; :: thesis: ( len u < len w & len v < len w )
A4: len w = (len u) + (len v) by A1, AFINSQ_1:17;
then (len w) + (len u) > ((len u) + (len v)) + 0 by A2, XREAL_1:8;
hence ( len u < len w & len v < len w ) by A3, A4, XREAL_1:6, XREAL_1:8; :: thesis: verum