deffunc H1( 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 = H1(x) from PBOOLE:sch 4();
 X is V2()
proof
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 = H1(x) by A1;
hence not X . x is empty ; :: thesis: verum
end;
then reconsider X = X as V2() ManySortedSet of the carrier of S ;
deffunc H2( 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 = H2(x) from PBOOLE:sch 4();
 ch is Function-yielding
proof
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 = H2(x) by A2;
hence ch . x is set ; :: thesis: verum
end;
then reconsider ch = ch as ManySortedFunction of the carrier' of S ;
the Sorts of A is ManySortedSubset of X
proof
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 = H1(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;
then reconsider Y = the Sorts of A as ManySortedSubset of X ;
X is ManySortedSubset of X
proof
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;
then reconsider X1 = X as ManySortedSubset of X ;
ch is ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S
proof
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 = H2(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 H2(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 H2(x) c= (X * the ResultSort of S) . x & ch . x = H2(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;
then reconsider ch = ch as ManySortedFunction of (X #) * the Arity of S,X * the ResultSort of S ;
the Sorts of A is ManySortedElement of X
proof
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 = H1(x) by A1;
hence the Sorts of A . x is Element of X . x by ORDINAL1:8; :: thesis: verum
end;
then reconsider u = the Sorts of A as ManySortedElement of X ;
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 )
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
A10: now :: thesis: not p in Args (o,A)
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;
let b be Element of B,(the_result_sort_of o); :: thesis: ( b = (Den (o,B)) . p implies 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 = H2(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;
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 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 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
let 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;
thus the Sorts of B is V2() ; :: according to MSUALG_1:def 3 :: thesis: verum
thus verum ; :: thesis: verum