let a, b be Ordinal; :: thesis: 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 )
let S be Sequence; :: thesis: ( dom S = a +^ b implies ex S1, S2 being Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b ) )
assume A1: dom S = a +^ b ; :: thesis: ex S1, S2 being Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
set S1 = S | a;
A2: a c= a +^ b by ORDINAL3:24;
then A3: dom (S | a) = a by A1, RELAT_1:62;
deffunc H₁( Ordinal) -> set = S . (a +^ $1);
consider S2 being Sequence such that
A4: ( dom S2 = b & ( for c being Ordinal st c in b holds
S2 . c = H₁(c) ) ) from ORDINAL2:sch 2();
take S | a ; :: thesis: ex S2 being 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;
A5: dom S = dom ((S | a) ^ S2) by A1, A3, A4, ORDINAL4:def 1;

now :: thesis: for x being object st x in dom S holds
S . x = ((S | a) ^ S2) . x

let x be object ; :: thesis: ( x in dom S implies S . b₁ = ((S | a) ^ S2) . b₁ )
assume A6: 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 st
( c in b & z = a +^ c ) ) by A1, A6, ORDINAL3:38;

suppose A7: 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 A7, A3, ORDINAL4:def 1 ;
:: thesis: verum

end;

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

then consider c being Ordinal such that
A8: ( c in b & z = a +^ c ) ;
thus S . x = S2 . c by A4, A8
.= ((S | a) ^ S2) . x by A8, A3, A4, ORDINAL4:def 1 ; :: thesis: verum

end;

end;

end;

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