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 numbering (X \/ Y) = (numbering X) ^ (numbering Y) )
assume Z0: for x, y being set st x in X & y in Y holds
x in y ; :: thesis: numbering (X \/ Y) = (numbering X) ^ (numbering Y)
set f = numbering X;
set g = numbering Y;
set h = numbering (X \/ Y);
set a = ord-type X;
set b = ord-type Y;
set P = RelIncl ((ord-type X) +^ (ord-type Y));
set Q = RelIncl (X \/ Y);
set R = RelIncl (ord-type (X \/ Y));
A0: ( On (X \/ Y) = X \/ Y & On X = X & On Y = Y ) by EXCH10;
then I1: numbering (X \/ Y) is_isomorphism_of RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) by ThN3;
II: (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) by Z0, ThN6;
then I2: ( RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) are_isomorphic & RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) are_isomorphic ) by I1, WELLORD1:def 8;
then RelIncl (X \/ Y), RelIncl (ord-type (X \/ Y)) are_isomorphic by WELLORD1:40;
then (ord-type X) +^ (ord-type Y) = ord-type (X \/ Y) by I2, WELLORD1:42, WELLORD2:10;
hence numbering (X \/ Y) = (numbering X) ^ (numbering Y) by A0, II, I2, WELLORD1:def 9; :: thesis: verum