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 A1: 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:24;
then A2: dom (S | a) = a by A1, RELAT_1:62;
deffunc H₁( Ordinal) -> set = S . (a +^ $1);
consider S2 being T-Sequence such that
A3: ( 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;
A4: dom S = dom ((S | a) ^ S2) by A1, A2, A3, ORDINAL4:def 1;

now

let x be set ; :: thesis: ( x in dom S implies S . b₁ = ((S | a) ^ S2) . b₁ )
assume A5: 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 A1, A5, ORDINAL3:38;

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

hence S . x = (S | a) . z by FUNCT_1:49
.= ((S | a) ^ S2) . x by A6, A2, 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
A7: ( c in b & z = a +^ c ) ;
thus S . x = S2 . c by A3, A7
.= ((S | a) ^ S2) . x by A7, A2, A3, ORDINAL4:def 1 ; :: thesis: verum

end;

end;

end;

hence ( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b ) by A2, A3, A4, FUNCT_1:2; :: thesis: verum