defpred S1[ object , object ] means \$2 = max ((b1 . \$1),(b2 . \$1));
A1: for x being object st x in X holds
ex y being object st S1[x,y] ;
consider b being Function such that
A2: ( dom b = X & ( for x being object st x in X holds
S1[x,b . x] ) ) from reconsider b = b as ManySortedSet of X by ;
now :: thesis: for u being object st u in rng b holds
u in NAT
let u be object ; :: thesis: ( u in rng b implies u in NAT )
assume u in rng b ; :: thesis:
then consider x being object such that
A3: ( x in dom b & u = b . x ) by FUNCT_1:def 3;
u = max ((b1 . x),(b2 . x)) by A2, A3;
hence u in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then A4: rng b c= NAT by TARSKI:def 3;
now :: thesis: for u being object st u in support b holds
u in (support b1) \/ (support b2)
end;
then support b c= (support b1) \/ (support b2) by TARSKI:def 3;
then reconsider b = b as bag of X by ;
A10: dom b = X by PARTFUN1:def 2
.= dom b2 by PARTFUN1:def 2 ;
take b ; :: thesis: for k being object holds b . k = max ((b1 . k),(b2 . k))
A11: dom b = X by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2 ;
now :: thesis: for k being object holds b . k = max ((b1 . k),(b2 . k))
let k be object ; :: thesis: b . k = max ((b1 . k),(b2 . k))
now :: thesis: ( ( k in dom b & b . k = max ((b1 . k),(b2 . k)) ) or ( not k in dom b & b . k = max ((b1 . k),(b2 . k)) ) )
per cases ( k in dom b or not k in dom b ) ;
case k in dom b ; :: thesis: b . k = max ((b1 . k),(b2 . k))
hence b . k = max ((b1 . k),(b2 . k)) by A2; :: thesis: verum
end;
case A12: not k in dom b ; :: thesis: b . k = max ((b1 . k),(b2 . k))
then ( b1 . k = 0 & b2 . k = 0 ) by ;
hence b . k = max ((b1 . k),(b2 . k)) by ; :: thesis: verum
end;
end;
end;
hence b . k = max ((b1 . k),(b2 . k)) ; :: thesis: verum
end;
hence for k being object holds b . k = max ((b1 . k),(b2 . k)) ; :: thesis: verum