let A, B, C be Ordinal; :: thesis: (A +^ B) +^ C = A +^ (B +^ C)
defpred S₁[ Ordinal] means (A +^ B) +^ $1 = A +^ (B +^ $1);
A1: for C being Ordinal st S₁[C] holds
S₁[ succ C]

proof

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

end;

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

proof

deffunc H₁( Ordinal) -> set = (A +^ B) +^ $1;
let C be Ordinal; :: thesis: ( C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
S₁[D] ) implies S₁[C] )
assume that
A4: C <> 0 and
A5: C is limit_ordinal and
A6: for D being Ordinal st D in C holds
S₁[D] ; :: thesis: S₁[C]
consider L being Ordinal-Sequence such that
A7: ( dom L = C & ( for D being Ordinal st D in C holds
L . D = H₁(D) ) ) from ORDINAL2:sch 3();
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();
A9: rng L c= rng L1

proof

let x be object ; :: 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 object such that
A10: y in dom L and
A11: x = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A10;
A12: B +^ y in B +^ C by A7, A10, ORDINAL2:32;
L . y = (A +^ B) +^ y by A7, A10;
then A13: L . y = A +^ (B +^ y) by A6, A7, A10;
L1 . (B +^ y) = A +^ (B +^ y) by A7, A8, A10, ORDINAL2:32;
hence x in rng L1 by A8, A11, A13, A12, FUNCT_1:def 3; :: thesis: verum

end;

A14: B +^ C <> {} by A4, Th26;
B +^ C is limit_ordinal by A4, A5, Th29;
then A15: A +^ (B +^ C) = sup L1 by A8, A14, ORDINAL2:29
.= sup (rng L1) ;
(A +^ B) +^ C = sup L by A4, A5, A7, ORDINAL2:29
.= sup (rng L) ;
hence (A +^ B) +^ C c= A +^ (B +^ C) by A15, A9, ORDINAL2:22; :: according to XBOOLE_0:def 10 :: thesis: A +^ (B +^ C) c= (A +^ B) +^ C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A +^ (B +^ C) or x in (A +^ B) +^ C )
assume A16: x in A +^ (B +^ C) ; :: thesis: x in (A +^ B) +^ C
then reconsider x9 = x as Ordinal ;

A17: now :: thesis: ( not x in A +^ B implies x in (A +^ B) +^ C )

A18: A c= A +^ B by Th24;
assume A19: not x in A +^ B ; :: thesis: x in (A +^ B) +^ C
then A +^ B c= x9 by ORDINAL1:16;
then consider E being Ordinal such that
A20: x9 = A +^ E by A18, Th27, XBOOLE_1:1;
B c= E by A19, A20, ORDINAL1:16, ORDINAL2:32;
then consider F being Ordinal such that
A21: E = B +^ F by Th27;

A22: now :: thesis: F in C

assume not F in C ; :: thesis: contradiction
then B +^ C c= B +^ F by ORDINAL1:16, ORDINAL2:33;
then A +^ (B +^ C) c= A +^ (B +^ F) by ORDINAL2:33;
then x9 in x9 by A16, A20, A21;
hence contradiction ; :: thesis: verum

end;

then x = (A +^ B) +^ F by A6, A20, A21;
hence x in (A +^ B) +^ C by A22, ORDINAL2:32; :: thesis: verum

end;

A23: (A +^ B) +^ {} = A +^ B by ORDINAL2:27;
(A +^ B) +^ {} c= (A +^ B) +^ C by ORDINAL2:33, XBOOLE_1:2;
hence x in (A +^ B) +^ C by A23, A17; :: thesis: verum

end;

(A +^ B) +^ {} = A +^ B by ORDINAL2:27
.= A +^ (B +^ {}) by ORDINAL2:27 ;
then A24: S₁[ 0 ] ;
for C being Ordinal holds S₁[C] from ORDINAL2:sch 1(A24, A1, A3);
hence (A +^ B) +^ C = A +^ (B +^ C) ; :: thesis: verum