let E be non empty set ; :: thesis: for w, u, v being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds
( len u < len w & len v < len w )
let w, u, v 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 & v <> <%> E ) ; :: thesis: ( len u < len w & len v < len w )
len w = (len u) + (len v) by A1, AFINSQ_1:20;
then ( (len w) + (len u) > ((len u) + (len v)) + 0 & (len w) + (len v) > ((len u) + (len v)) + 0 ) by A2, XREAL_1:10;
hence ( len u < len w & len v < len w ) by XREAL_1:8; :: thesis: verum