defpred S₁[ object , object ] means $2 = max ((b1 . $1),(b2 . $1));
A1: for x being object st x in X holds
ex y being object st S₁[x,y] ;
consider b being Function such that
A2: ( dom b = X & ( for x being object st x in X holds
S₁[x,b . x] ) ) from CLASSES1:sch 1(A1);
reconsider b = b as ManySortedSet of X by A2, PARTFUN1:def 2, RELAT_1:def 18;

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: u in NAT
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)

let u be object ; :: thesis: ( u in support b implies u in (support b1) \/ (support b2) )
A5: support b c= dom b by PRE_POLY:37;
assume A6: u in support b ; :: thesis: u in (support b1) \/ (support b2)
then A7: b . u <> 0 by PRE_POLY:def 7;

now :: thesis: u in (support b1) \/ (support b2)

assume A8: not u in (support b1) \/ (support b2) ; :: thesis: contradiction
then not u in support b2 by XBOOLE_0:def 3;
then A9: b2 . u = 0 by PRE_POLY:def 7;
not u in support b1 by A8, XBOOLE_0:def 3;
then b1 . u = 0 by PRE_POLY:def 7;
then max ((b1 . u),(b2 . u)) = 0 by A9;
hence contradiction by A2, A6, A7, A5; :: thesis: verum

end;

hence u in (support b1) \/ (support b2) ; :: thesis: verum

end;

then support b c= (support b1) \/ (support b2) by TARSKI:def 3;
then reconsider b = b as bag of X by A4, PRE_POLY:def 8, VALUED_0:def 6;
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 A11, A10, FUNCT_1:def 2;
hence b . k = max ((b1 . k),(b2 . k)) by A12, FUNCT_1:def 2; :: 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