for a, b being Ordinal
for S being Sequence st dom S = a +^ b holds
ex S1, S2 being Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )