deffunc H_{1}( object ) -> set = succ ( the Sorts of A . S);

consider X being ManySortedSet of the carrier of S such that

A1: for x being object st x in the carrier of S holds

X . x = H_{1}(x)
from PBOOLE:sch 4();

X is V2()

deffunc H_{2}( object ) -> set = ((((X #) * the Arity of S) . S) --> (( the Sorts of A * the ResultSort of S) . S)) +* ( the Charact of A . S);

consider ch being ManySortedSet of the carrier' of S such that

A2: for x being object st x in the carrier' of S holds

ch . x = H_{2}(x)
from PBOOLE:sch 4();

ch is Function-yielding

the Sorts of A is ManySortedSubset of X

X is ManySortedSubset of X

ch is ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S

the Sorts of A is ManySortedElement of X

take B = UndefMSAlgebra(# X,ch,u #); :: thesis: ( B is A -undef & B is non-empty )

for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

thus for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) by A1; :: thesis: ( ( for o being OperSymbol of S

for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

thus verum ; :: thesis: verum

consider X being ManySortedSet of the carrier of S such that

A1: for x being object st x in the carrier of S holds

X . x = H

X is V2()

proof

then reconsider X = X as V2() ManySortedSet of the carrier of S ;
let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in the carrier of S or not X . x is empty )

assume x in the carrier of S ; :: thesis: not X . x is empty

then X . x = H_{1}(x)
by A1;

hence not X . x is empty ; :: thesis: verum

end;assume x in the carrier of S ; :: thesis: not X . x is empty

then X . x = H

hence not X . x is empty ; :: thesis: verum

deffunc H

consider ch being ManySortedSet of the carrier' of S such that

A2: for x being object st x in the carrier' of S holds

ch . x = H

ch is Function-yielding

proof

then reconsider ch = ch as ManySortedFunction of the carrier' of S ;
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 ch or ch . x is set )

assume x in dom ch ; :: thesis: ch . x is set

then x in the carrier' of S by PARTFUN1:def 2;

then ch . x = H_{2}(x)
by A2;

hence ch . x is set ; :: thesis: verum

end;assume x in dom ch ; :: thesis: ch . x is set

then x in the carrier' of S by PARTFUN1:def 2;

then ch . x = H

hence ch . x is set ; :: thesis: verum

the Sorts of A is ManySortedSubset of X

proof

then reconsider Y = the Sorts of A as ManySortedSubset of X ;
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or the Sorts of A . x c= X . x )

assume x in the carrier of S ; :: thesis: the Sorts of A . x c= X . x

then X . x = H_{1}(x)
by A1

.= ( the Sorts of A . x) \/ {( the Sorts of A . x)} ;

hence the Sorts of A . x c= X . x by XBOOLE_1:7; :: thesis: verum

end;assume x in the carrier of S ; :: thesis: the Sorts of A . x c= X . x

then X . x = H

.= ( the Sorts of A . x) \/ {( the Sorts of A . x)} ;

hence the Sorts of A . x c= X . x by XBOOLE_1:7; :: thesis: verum

X is ManySortedSubset of X

proof

then reconsider X1 = X as ManySortedSubset of X ;
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or X . x c= X . x )

thus ( not x in the carrier of S or X . x c= X . x ) ; :: thesis: verum

end;thus ( not x in the carrier of S or X . x c= X . x ) ; :: thesis: verum

ch is ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S

proof

then reconsider ch = ch as ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S ;
let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier' of S or ch . x is Element of bool [:(((X #) * the Arity of S) . x),((X * the ResultSort of S) . x):] )

assume x in the carrier' of S ; :: thesis: ch . x is Element of bool [:(((X #) * the Arity of S) . x),((X * the ResultSort of S) . x):]

then reconsider x = x as OperSymbol of S ;

( Y # c= X # & the_arity_of x in the carrier of S * & dom the Arity of S = the carrier' of S & the Charact of A is ManySortedFunction of (Y #) * the Arity of S,Y * the ResultSort of S ) by Th2, FUNCT_2:def 1, PBOOLE:def 18;

then ( (Y #) . (the_arity_of x) c= (X #) . (the_arity_of x) & ((Y #) * the Arity of S) . x = (Y #) . (the_arity_of x) & ((X1 #) * the Arity of S) . x = (X #) . (the_arity_of x) & the Charact of A . x is Function of (((Y #) * the Arity of S) . x),((Y * the ResultSort of S) . x) ) by FUNCT_1:13;

then ( (((X #) * the Arity of S) . x) \/ (((Y #) * the Arity of S) . x) = ((X #) * the Arity of S) . x & dom ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x)) = ((X #) * the Arity of S) . x & dom ( the Charact of A . x) = ((Y #) * the Arity of S) . x & ch . x = H_{2}(x) )
by A2, XBOOLE_1:12, FUNCT_2:def 1;

then A3: dom (ch . x) = ((X #) * the Arity of S) . x by FUNCT_4:def 1;

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

then A4: ( (Y * the ResultSort of S) . x = Y . (the_result_sort_of x) & (X * the ResultSort of S) . x = X . (the_result_sort_of x) ) by FUNCT_1:13;

then A5: (Y * the ResultSort of S) . x c= (X * the ResultSort of S) . x by PBOOLE:def 18, PBOOLE:def 2;

X . (the_result_sort_of x) = succ (Y . (the_result_sort_of x)) by A1;

then Y . (the_result_sort_of x) in X . (the_result_sort_of x) by ORDINAL1:8;

then {(Y . (the_result_sort_of x))} c= X . (the_result_sort_of x) by ZFMISC_1:31;

then A6: rng ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x)) c= X . (the_result_sort_of x) by A4;

rng ( the Charact of A . x) c= X . (the_result_sort_of x) by A5, A4, RELAT_1:def 19;

then A7: (rng ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x))) \/ (rng ( the Charact of A . x)) c= X . (the_result_sort_of x) by A6, XBOOLE_1:8;

rng H_{2}(x) c= (rng ((((X #) * the Arity of S) . x) --> ((Y * the ResultSort of S) . x))) \/ (rng ( the Charact of A . x))
by FUNCT_4:17;

then ( rng H_{2}(x) c= (X * the ResultSort of S) . x & ch . x = H_{2}(x) )
by A2, A4, A7;

hence ch . x is Element of bool [:(((X #) * the Arity of S) . x),((X * the ResultSort of S) . x):] by A3, FUNCT_2:2; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: ch . x is Element of bool [:(((X #) * the Arity of S) . x),((X * the ResultSort of S) . x):]

then reconsider x = x as OperSymbol of S ;

( Y # c= X # & the_arity_of x in the carrier of S * & dom the Arity of S = the carrier' of S & the Charact of A is ManySortedFunction of (Y #) * the Arity of S,Y * the ResultSort of S ) by Th2, FUNCT_2:def 1, PBOOLE:def 18;

then ( (Y #) . (the_arity_of x) c= (X #) . (the_arity_of x) & ((Y #) * the Arity of S) . x = (Y #) . (the_arity_of x) & ((X1 #) * the Arity of S) . x = (X #) . (the_arity_of x) & the Charact of A . x is Function of (((Y #) * the Arity of S) . x),((Y * the ResultSort of S) . x) ) by FUNCT_1:13;

then ( (((X #) * the Arity of S) . x) \/ (((Y #) * the Arity of S) . x) = ((X #) * the Arity of S) . x & dom ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x)) = ((X #) * the Arity of S) . x & dom ( the Charact of A . x) = ((Y #) * the Arity of S) . x & ch . x = H

then A3: dom (ch . x) = ((X #) * the Arity of S) . x by FUNCT_4:def 1;

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

then A4: ( (Y * the ResultSort of S) . x = Y . (the_result_sort_of x) & (X * the ResultSort of S) . x = X . (the_result_sort_of x) ) by FUNCT_1:13;

then A5: (Y * the ResultSort of S) . x c= (X * the ResultSort of S) . x by PBOOLE:def 18, PBOOLE:def 2;

X . (the_result_sort_of x) = succ (Y . (the_result_sort_of x)) by A1;

then Y . (the_result_sort_of x) in X . (the_result_sort_of x) by ORDINAL1:8;

then {(Y . (the_result_sort_of x))} c= X . (the_result_sort_of x) by ZFMISC_1:31;

then A6: rng ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x)) c= X . (the_result_sort_of x) by A4;

rng ( the Charact of A . x) c= X . (the_result_sort_of x) by A5, A4, RELAT_1:def 19;

then A7: (rng ((((X #) * the Arity of S) . x) --> (( the Sorts of A * the ResultSort of S) . x))) \/ (rng ( the Charact of A . x)) c= X . (the_result_sort_of x) by A6, XBOOLE_1:8;

rng H

then ( rng H

hence ch . x is Element of bool [:(((X #) * the Arity of S) . x),((X * the ResultSort of S) . x):] by A3, FUNCT_2:2; :: thesis: verum

the Sorts of A is ManySortedElement of X

proof

then reconsider u = the Sorts of A as ManySortedElement of X ;
let x be set ; :: according to AOFA_A00:def 12 :: thesis: ( x in the carrier of S implies the Sorts of A . x is Element of X . x )

assume x in the carrier of S ; :: thesis: the Sorts of A . x is Element of X . x

then X . x = H_{1}(x)
by A1;

hence the Sorts of A . x is Element of X . x by ORDINAL1:8; :: thesis: verum

end;assume x in the carrier of S ; :: thesis: the Sorts of A . x is Element of X . x

then X . x = H

hence the Sorts of A . x is Element of X . x by ORDINAL1:8; :: thesis: verum

take B = UndefMSAlgebra(# X,ch,u #); :: thesis: ( B is A -undef & B is non-empty )

hereby :: according to AOFA_A00:def 14,AOFA_A00:def 15 :: thesis: ( the undefined-map of B = the Sorts of A & ( for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) ) & ( for o being OperSymbol of S

for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

thus
the undefined-map of B = the Sorts of A
; :: thesis: ( ( for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) ) & ( for o being OperSymbol of Sfor a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

let o be OperSymbol of S; :: thesis: for p being FinSequence st p in Args (o,B) & ex i being Nat ex s being SortSymbol of S ex a being Element of B,s st

( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined

let p be FinSequence; :: thesis: ( p in Args (o,B) & ex i being Nat ex s being SortSymbol of S ex a being Element of B,s st

( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) implies for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined )

assume A8: p in Args (o,B) ; :: thesis: ( ex i being Nat ex s being SortSymbol of S ex a being Element of B,s st

( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) implies for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined )

given i being Nat, s being SortSymbol of S, a being Element of B,s such that A9: ( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) ; :: thesis: for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined

assume A13: b = (Den (o,B)) . p ; :: thesis: b is undefined

A14: dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;

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

b = H_{2}(o) . p
by A2, A13

.= ((Args (o,B)) --> ((Y * the ResultSort of S) . o)) . p by A14, A10, FUNCT_4:11

.= (Y * the ResultSort of S) . o by A8, FUNCOP_1:7

.= u . (the_result_sort_of o) by A15, FUNCT_1:13 ;

hence b is undefined ; :: thesis: verum

end;( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds

for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined

let p be FinSequence; :: thesis: ( p in Args (o,B) & ex i being Nat ex s being SortSymbol of S ex a being Element of B,s st

( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) implies for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined )

assume A8: p in Args (o,B) ; :: thesis: ( ex i being Nat ex s being SortSymbol of S ex a being Element of B,s st

( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) implies for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined )

given i being Nat, s being SortSymbol of S, a being Element of B,s such that A9: ( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) ; :: thesis: for b being Element of B,(the_result_sort_of o) st b = (Den (o,B)) . p holds

b is undefined

A10: now :: thesis: not p in Args (o,A)

let b be Element of B,(the_result_sort_of o); :: thesis: ( b = (Den (o,B)) . p implies b is undefined )assume A11:
p in Args (o,A)
; :: thesis: contradiction

A12: dom (Y * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;

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

then Args (o,A) = (Y #) . (the_arity_of o) by FUNCT_1:13

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

then p . i in (Y * (the_arity_of o)) . i by A9, A11, A12, CARD_3:9;

then ( a in Y . s & u . s = a ) by A9, FUNCT_1:13;

hence contradiction ; :: thesis: verum

end;A12: dom (Y * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;

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

then Args (o,A) = (Y #) . (the_arity_of o) by FUNCT_1:13

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

then p . i in (Y * (the_arity_of o)) . i by A9, A11, A12, CARD_3:9;

then ( a in Y . s & u . s = a ) by A9, FUNCT_1:13;

hence contradiction ; :: thesis: verum

assume A13: b = (Den (o,B)) . p ; :: thesis: b is undefined

A14: dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;

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

b = H

.= ((Args (o,B)) --> ((Y * the ResultSort of S) . o)) . p by A14, A10, FUNCT_4:11

.= (Y * the ResultSort of S) . o by A8, FUNCOP_1:7

.= u . (the_result_sort_of o) by A15, FUNCT_1:13 ;

hence b is undefined ; :: thesis: verum

for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

thus for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) by A1; :: thesis: ( ( for o being OperSymbol of S

for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) & B is non-empty )

hereby :: thesis: B is non-empty

thus
the Sorts of B is V2()
; :: according to MSUALG_1:def 3 :: thesis: verumlet o be OperSymbol of S; :: thesis: for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds

(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o)

let a be Element of Args (o,A); :: thesis: ( Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a implies (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) )

assume Args (o,A) <> {} ; :: thesis: ( (Den (o,B)) . a <> (Den (o,A)) . a implies (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) )

assume A16: (Den (o,B)) . a <> (Den (o,A)) . a ; :: thesis: (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o)

A17: dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;

(Den (o,B)) . a = (((((X #) * the Arity of S) . o) --> (( the Sorts of A * the ResultSort of S) . o)) +* ( the Charact of A . o)) . a by A2

.= (Den (o,A)) . a by A17, FUNCT_4:13 ;

hence (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) by A16; :: thesis: verum

end;(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o)

let a be Element of Args (o,A); :: thesis: ( Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a implies (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) )

assume Args (o,A) <> {} ; :: thesis: ( (Den (o,B)) . a <> (Den (o,A)) . a implies (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) )

assume A16: (Den (o,B)) . a <> (Den (o,A)) . a ; :: thesis: (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o)

A17: dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;

(Den (o,B)) . a = (((((X #) * the Arity of S) . o) --> (( the Sorts of A * the ResultSort of S) . o)) +* ( the Charact of A . o)) . a by A2

.= (Den (o,A)) . a by A17, FUNCT_4:13 ;

hence (Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) by A16; :: thesis: verum

thus verum ; :: thesis: verum