let E be set ; :: thesis: for b being Element of E ^omega
for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
let b be Element of E ^omega ; :: thesis: for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
let n, m be Nat; :: thesis: ( len b = n + m implies ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 ) )
assume len b = n + m ; :: thesis: ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
then consider c19, c29 being XFinSequence such that
A1: ( len c19 = n & len c29 = m ) and
A2: b = c19 ^ c29 by Lm1;
reconsider c2 = c29 as Element of E ^omega by A2, Th5;
reconsider c1 = c19 as Element of E ^omega by A2, Th5;
take c1 ; :: thesis: ex c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
take c2 ; :: thesis: ( len c1 = n & len c2 = m & b = c1 ^ c2 )
thus ( len c1 = n & len c2 = m & b = c1 ^ c2 ) by A1, A2; :: thesis: verum