let X be set ; :: thesis: for v being Element of (free_magma X) st not X is empty holds
( v = [(v `1),(v `2)] & length v >= 1 )
let v be Element of (free_magma X); :: thesis: ( not X is empty implies ( v = [(v `1),(v `2)] & length v >= 1 ) )
assume not X is empty ; :: thesis: ( v = [(v `1),(v `2)] & length v >= 1 )
then reconsider X9 = X as non empty set ;
reconsider v9 = v as Element of (free_magma X9) ;
v9 in [:(free_magma (X,(v9 `2))),{(v9 `2)}:] by Th25;
then ex x, y being object st
( x in free_magma (X,(v9 `2)) & y in {(v9 `2)} & v9 = [x,y] ) by ZFMISC_1:def 2;
hence v = [(v `1),(v `2)] ; :: thesis: length v >= 1
reconsider v99 = v9 as Element of free_magma_carrier X9 ;
v99 `2 > 0 ;
then length v9 > 0 by Def18;
then (length v9) + 1 > 0 + 1 by XREAL_1:6;
hence length v >= 1 by NAT_1:13; :: thesis: verum