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 c1', c2' being XFinSequence such that
A1: ( len c1' = n & len c2' = m ) and
A2: b = c1' ^ c2' by Th10;
reconsider c2 = c2' as Element of E ^omega by A2, Th5;
reconsider c1 = c1' 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