let E be non empty set ; :: thesis: for u being Element of E ^omega
for k being Nat st k <> 0 & len u <= k + 1 holds
ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )
let u be Element of E ^omega ; :: thesis: for k being Nat st k <> 0 & len u <= k + 1 holds
ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )
let k be Nat; :: thesis: ( k <> 0 & len u <= k + 1 implies ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) )
assume that
A1: k <> 0 and
A2: len u <= k + 1 ; :: thesis: ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )

per cases ( len u = k + 1 or len u <> k + 1 ) ;

suppose len u = k + 1 ; :: thesis: ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )

then consider v1 being Element of E ^omega , e being Element of E such that
A3: len v1 = k and
A4: u = v1 ^ <%e%> by FLANG_1:7;
reconsider v2 = <%e%> as Element of E ^omega ;
take v1 ; :: thesis: ex v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )
take v2 ; :: thesis: ( len v1 <= k & len v2 <= k & u = v1 ^ v2 )
thus len v1 <= k by A3; :: thesis: ( len v2 <= k & u = v1 ^ v2 )
0 + 1 <= k by A1, NAT_1:13;
hence len v2 <= k by AFINSQ_1:34; :: thesis: u = v1 ^ v2
thus u = v1 ^ v2 by A4; :: thesis: verum

end;

suppose A5: len u <> k + 1 ; :: thesis: ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )

reconsider v2 = <%> E as Element of E ^omega ;
take u ; :: thesis: ex v2 being Element of E ^omega st
( len u <= k & len v2 <= k & u = u ^ v2 )
take v2 ; :: thesis: ( len u <= k & len v2 <= k & u = u ^ v2 )
thus len u <= k by A2, A5, NAT_1:8; :: thesis: ( len v2 <= k & u = u ^ v2 )
thus len v2 <= k ; :: thesis: u = u ^ v2
thus u = u ^ {}
.= u ^ v2 ; :: thesis: verum

end;

end;