let X be set ; :: thesis: for v being Element of st not X is empty holds
( v = [(v `1 ),(v `2 )] & length v >= 1 )
let v be Element of ; :: 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 X' = X as non empty set ;
reconsider v' = v as Element of ;
v' in [:(free_magma X,(v' `2 )),{(v' `2 )}:] by Th25;
then ex x, y being set st
( x in free_magma X,(v' `2 ) & y in {(v' `2 )} & v' = [x,y] ) by ZFMISC_1:def 2;
hence v = [(v `1 ),(v `2 )] by MCART_1:8; :: thesis: length v >= 1
reconsider v'' = v' as Element of free_magma_carrier X' ;
v'' `2 > 0 ;
then length v' > 0 by Def19;
then (length v') + 1 > 0 + 1 by XREAL_1:8;
hence length v >= 1 by NAT_1:13; :: thesis: verum