let X, Y be ordinal-membered set ; :: thesis: ( ( for x, y being set st x in X & y in Y holds
x in y ) implies ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y) )
assume for x, y being set st x in X & y in Y holds
x in y ; :: thesis: ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)
then A1: numbering (X \/ Y) = (numbering X) ^ (numbering Y) by Th25;
thus ord-type (X \/ Y) = dom (numbering (X \/ Y)) by Th18
.= (dom (numbering X)) +^ (dom (numbering Y)) by A1, ORDINAL4:def 1
.= (ord-type X) +^ (dom (numbering Y)) by Th18
.= (ord-type X) +^ (ord-type Y) by Th18 ; :: thesis: verum