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