defpred S_{1}[ 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_{1}[x,y]
;

consider b being Function such that

A2: ( dom b = X & ( for x being object st x in X holds

S_{1}[x,b . x] ) )
from CLASSES1:sch 1(A1);

reconsider b = b as ManySortedSet of X by A2, PARTFUN1:def 2, RELAT_1:def 18;

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 ;

A1: for x being object st x in X holds

ex y being object st S

consider b being Function such that

A2: ( dom b = X & ( for x being object st x in X holds

S

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

then A4:
rng b c= NAT
by TARSKI:def 3;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;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

now :: thesis: for u being object st u in support b holds

u in (support b1) \/ (support b2)

then
support b c= (support b1) \/ (support b2)
by TARSKI:def 3;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;

end;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)

hence
u in (support b1) \/ (support b2)
; :: thesis: verumassume 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;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

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))

hence
for k being object holds b . k = max ((b1 . k),(b2 . k))
; :: thesis: verumlet k be object ; :: thesis: b . k = max ((b1 . k),(b2 . k))

end;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)) ) )

hence
b . k = max ((b1 . k),(b2 . k))
; :: thesis: verumend;