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 A1: 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));
A2: ( On (X \/ Y) = X \/ Y & On X = X & On Y = Y ) by Th2;
then A3: numbering (X \/ Y) is_isomorphism_of RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) by Th21;
A4: (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) by A1, Th24;
then A5: ( RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) are_isomorphic & RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) are_isomorphic ) by A3;
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 A5, WELLORD1:42, WELLORD2:10;
hence numbering (X \/ Y) = (numbering X) ^ (numbering Y) by A2, A4, A5, WELLORD1:def 9; :: thesis: verum