let A, B, C be Ordinal; :: thesis: (A +^ B) +^ C = A +^ (B +^ C)
defpred S₁[ Ordinal] means (A +^ B) +^ $1 = A +^ (B +^ $1);
A1: S₁[ {} ]

proof

thus (A +^ B) +^ {} = A +^ B by ORDINAL2:44
.= A +^ (B +^ {} ) by ORDINAL2:44 ; :: thesis: verum

end;

A2: for C being Ordinal st S₁[C] holds
S₁[ succ C]

proof

let C be Ordinal; :: thesis: ( S₁[C] implies S₁[ succ C] )
assume A3: (A +^ B) +^ C = A +^ (B +^ C) ; :: thesis: S₁[ succ C]
thus (A +^ B) +^ (succ C) = succ ((A +^ B) +^ C) by ORDINAL2:45
.= A +^ (succ (B +^ C)) by A3, ORDINAL2:45
.= A +^ (B +^ (succ C)) by ORDINAL2:45 ; :: thesis: verum

end;

A4: for C being Ordinal st C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) holds
S₁[C]

proof

let C be Ordinal; :: thesis: ( C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) implies S₁[C] )
assume A5: ( C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) ) ; :: thesis: S₁[C]
deffunc H₁( Ordinal) -> set = (A +^ B) +^ $1;
consider L being Ordinal-Sequence such that
A6: ( dom L = C & ( for D being Ordinal st D in C holds
L . D = H₁(D) ) ) from ORDINAL2:sch 3();
A7: (A +^ B) +^ C = sup L by A5, A6, ORDINAL2:46
.= sup (rng L) ;
deffunc H₂( Ordinal) -> set = A +^ $1;
consider L1 being Ordinal-Sequence such that
A8: ( dom L1 = B +^ C & ( for D being Ordinal st D in B +^ C holds
L1 . D = H₂(D) ) ) from ORDINAL2:sch 3();
( B +^ C is limit_ordinal & B +^ C <> {} ) by A5, Th29, Th32;
then A9: A +^ (B +^ C) = sup L1 by A8, ORDINAL2:46
.= sup (rng L1) ;
rng L c= rng L1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in rng L1 )
assume x in rng L ; :: thesis: x in rng L1
then consider y being set such that
A10: ( y in dom L & x = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A10;
( L . y = (A +^ B) +^ y & S₁[y] ) by A5, A6, A10;
then A11: ( L . y = A +^ (B +^ y) & B +^ y in B +^ C ) by A6, A10, ORDINAL2:49;
then L1 . (B +^ y) = A +^ (B +^ y) by A8;
hence x in rng L1 by A8, A10, A11, FUNCT_1:def 5; :: thesis: verum

end;

hence (A +^ B) +^ C c= A +^ (B +^ C) by A7, A9, ORDINAL2:30; :: according to XBOOLE_0:def 10 :: thesis: A +^ (B +^ C) c= (A +^ B) +^ C
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A +^ (B +^ C) or x in (A +^ B) +^ C )
assume A12: x in A +^ (B +^ C) ; :: thesis: x in (A +^ B) +^ C
then reconsider x' = x as Ordinal ;
{} c= C by XBOOLE_1:2;
then A13: ( (A +^ B) +^ {} c= (A +^ B) +^ C & (A +^ B) +^ {} = A +^ B ) by ORDINAL2:44, ORDINAL2:50;

now

assume A14: not x in A +^ B ; :: thesis: x in (A +^ B) +^ C
then ( A c= A +^ B & A +^ B c= x' ) by Th27, ORDINAL1:26;
then A c= x' by XBOOLE_1:1;
then consider E being Ordinal such that
A15: x' = A +^ E by Th30;
B c= E by A14, A15, ORDINAL1:26, ORDINAL2:49;
then consider F being Ordinal such that
A16: E = B +^ F by Th30;

now

assume not F in C ; :: thesis: contradiction
then B +^ C c= B +^ F by ORDINAL1:26, ORDINAL2:50;
then A +^ (B +^ C) c= A +^ (B +^ F) by ORDINAL2:50;
then x' in x' by A12, A15, A16;
hence contradiction ; :: thesis: verum

end;

then ( x = (A +^ B) +^ F & (A +^ B) +^ F in (A +^ B) +^ C ) by A5, A15, A16, ORDINAL2:49;
hence x in (A +^ B) +^ C ; :: thesis: verum

end;

hence x in (A +^ B) +^ C by A13; :: thesis: verum

end;

for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A1, A2, A4);
hence (A +^ B) +^ C = A +^ (B +^ C) ; :: thesis: verum