let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S

for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

let U0 be MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

let U1 be MSSubAlgebra of U0; :: thesis: Constants U0 is MSSubset of U1

Constants U0 c= the Sorts of U1

for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

let U0 be MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

let U1 be MSSubAlgebra of U0; :: thesis: Constants U0 is MSSubset of U1

Constants U0 c= the Sorts of U1

proof

hence
Constants U0 is MSSubset of U1
by PBOOLE:def 18; :: thesis: verum
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or (Constants U0) . x c= the Sorts of U1 . x )

assume x in the carrier of S ; :: thesis: (Constants U0) . x c= the Sorts of U1 . x

then reconsider s = x as SortSymbol of S ;

thus (Constants U0) . x c= the Sorts of U1 . x :: thesis: verum

end;assume x in the carrier of S ; :: thesis: (Constants U0) . x c= the Sorts of U1 . x

then reconsider s = x as SortSymbol of S ;

thus (Constants U0) . x c= the Sorts of U1 . x :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )

end;per cases
( the Sorts of U0 . s = {} or the Sorts of U0 . s <> {} )
;

end;

suppose A1:
the Sorts of U0 . s = {}
; :: thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )

(Constants U0) . s =
Constants (U0,s)
by Def4

.= {} by A1 ;

hence ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) ; :: thesis: verum

end;.= {} by A1 ;

hence ( not y in (Constants U0) . x or y in the Sorts of U1 . x ) ; :: thesis: verum

suppose
the Sorts of U0 . s <> {}
; :: thesis: ( not y in (Constants U0) . x or y in the Sorts of U1 . x )

then A2:
ex A being non empty set st

( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3;

reconsider u1 = the Sorts of U1 as MSSubset of U0 by Def9;

assume A3: y in (Constants U0) . x ; :: thesis: y in the Sorts of U1 . x

(Constants U0) . x = Constants (U0,s) by Def4;

then consider b being Element of the Sorts of U0 . s such that

A4: b = y and

A5: ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) by A3, A2;

consider o being OperSymbol of S such that

A6: the Arity of S . o = {} and

A7: the ResultSort of S . o = s and

A8: b in rng (Den (o,U0)) by A5;

A9: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;

then A10: the Arity of S . o in rng the Arity of S by FUNCT_1:def 3;

( dom {} = {} & rng {} = {} ) ;

then reconsider a = {} as Function of {},{} by FUNCT_2:1;

A11: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

dom (u1 #) = the carrier of S * by PARTFUN1:def 2;

then o in dom ((u1 #) * the Arity of S) by A9, A10, FUNCT_1:11;

then A12: ((u1 #) * the Arity of S) . o = (u1 #) . ( the Arity of S . o) by FUNCT_1:12

.= (u1 #) . (the_arity_of o) by MSUALG_1:def 1

.= product (u1 * (the_arity_of o)) by FINSEQ_2:def 5

.= product (u1 * a) by A6, MSUALG_1:def 1

.= {{}} by CARD_3:10 ;

dom ( the Sorts of U0 #) = the carrier of S * by PARTFUN1:def 2;

then A13: o in dom (( the Sorts of U0 #) * the Arity of S) by A9, A10, FUNCT_1:11;

u1 is opers_closed by Def9;

then u1 is_closed_on o ;

then A14: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o ;

rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def 19;

then dom (Den (o,U0)) = Args (o,U0) by A8, FUNCT_2:def 1

.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def 4

.= ( the Sorts of U0 #) . ( the Arity of S . o) by A13, FUNCT_1:12

.= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def 1

.= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def 5

.= product ( the Sorts of U0 * a) by A6, MSUALG_1:def 1

.= {{}} by CARD_3:10 ;

then (Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (o,U0) by A12;

then b in (u1 * the ResultSort of S) . o by A8, A14;

hence y in the Sorts of U1 . x by A4, A7, A11, FUNCT_1:13; :: thesis: verum

end;( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } ) by Def3;

reconsider u1 = the Sorts of U1 as MSSubset of U0 by Def9;

assume A3: y in (Constants U0) . x ; :: thesis: y in the Sorts of U1 . x

(Constants U0) . x = Constants (U0,s) by Def4;

then consider b being Element of the Sorts of U0 . s such that

A4: b = y and

A5: ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) by A3, A2;

consider o being OperSymbol of S such that

A6: the Arity of S . o = {} and

A7: the ResultSort of S . o = s and

A8: b in rng (Den (o,U0)) by A5;

A9: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;

then A10: the Arity of S . o in rng the Arity of S by FUNCT_1:def 3;

( dom {} = {} & rng {} = {} ) ;

then reconsider a = {} as Function of {},{} by FUNCT_2:1;

A11: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

dom (u1 #) = the carrier of S * by PARTFUN1:def 2;

then o in dom ((u1 #) * the Arity of S) by A9, A10, FUNCT_1:11;

then A12: ((u1 #) * the Arity of S) . o = (u1 #) . ( the Arity of S . o) by FUNCT_1:12

.= (u1 #) . (the_arity_of o) by MSUALG_1:def 1

.= product (u1 * (the_arity_of o)) by FINSEQ_2:def 5

.= product (u1 * a) by A6, MSUALG_1:def 1

.= {{}} by CARD_3:10 ;

dom ( the Sorts of U0 #) = the carrier of S * by PARTFUN1:def 2;

then A13: o in dom (( the Sorts of U0 #) * the Arity of S) by A9, A10, FUNCT_1:11;

u1 is opers_closed by Def9;

then u1 is_closed_on o ;

then A14: rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o ;

rng (Den (o,U0)) c= Result (o,U0) by RELAT_1:def 19;

then dom (Den (o,U0)) = Args (o,U0) by A8, FUNCT_2:def 1

.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def 4

.= ( the Sorts of U0 #) . ( the Arity of S . o) by A13, FUNCT_1:12

.= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def 1

.= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def 5

.= product ( the Sorts of U0 * a) by A6, MSUALG_1:def 1

.= {{}} by CARD_3:10 ;

then (Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (o,U0) by A12;

then b in (u1 * the ResultSort of S) . o by A8, A14;

hence y in the Sorts of U1 . x by A4, A7, A11, FUNCT_1:13; :: thesis: verum