let a, b be ordinal number ; :: thesis: for S being T-Sequence st dom S = a +^ b holds
ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
let S be T-Sequence; :: thesis: ( dom S = a +^ b implies ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b ) )
assume A0: dom S = a +^ b ; :: thesis: ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
set S1 = S | a;
a c= a +^ b by ORDINAL3:27;
then B1: dom (S | a) = a by A0, RELAT_1:91;
deffunc H₁( Ordinal) -> set = S . (a +^ $1);
consider S2 being T-Sequence such that
A1: ( dom S2 = b & ( for c being ordinal number st c in b holds
S2 . c = H₁(c) ) ) from ORDINAL2:sch 2();
take S | a ; :: thesis: ex S2 being T-Sequence st
( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b )
take S2 ; :: thesis: ( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b )
set s = (S | a) ^ S2;
A2: dom S = dom ((S | a) ^ S2) by A0, B1, A1, ORDINAL4:def 1;

now

let x be set ; :: thesis: ( x in dom S implies S . b₁ = ((S | a) ^ S2) . b₁ )
assume A3: x in dom S ; :: thesis: S . b₁ = ((S | a) ^ S2) . b₁
then reconsider z = x as Ordinal ;

per cases ( z in a or ex c being ordinal number st
( c in b & z = a +^ c ) ) by A0, A3, ORDINAL3:42;

suppose A4: z in a ; :: thesis: S . b₁ = ((S | a) ^ S2) . b₁

hence S . x = (S | a) . z by FUNCT_1:72
.= ((S | a) ^ S2) . x by A4, B1, ORDINAL4:def 1 ;
:: thesis: verum

end;

suppose ex c being ordinal number st
( c in b & z = a +^ c ) ; :: thesis: S . b₁ = ((S | a) ^ S2) . b₁

then consider c being ordinal number such that
A5: ( c in b & z = a +^ c ) ;
thus S . x = S2 . c by A1, A5
.= ((S | a) ^ S2) . x by A5, B1, A1, ORDINAL4:def 1 ; :: thesis: verum

end;

end;

end;

hence ( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b ) by B1, A1, A2, FUNCT_1:9; :: thesis: verum