deffunc H₁( 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₁(x) from PBOOLE:sch 4();
X is non-empty

proof

let x be object ; :: according to PBOOLE:def 13 :: thesis:
assume x in the carrier of S ; :: thesis:
then X . x = H₁(x) by A1;
hence not X . x is empty ; :: thesis:

end;

then reconsider X = X as non-empty ManySortedSet of the carrier of S ;
deffunc H₂( 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₂(x) from PBOOLE:sch 4();
ch is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume x in dom ch ; :: thesis:
then x in the carrier' of S by PARTFUN1:def 2;
then ch . x = H₂(x) by A2;
hence ch . x is set ; :: thesis:

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:
assume x in the carrier of S ; :: thesis:
then X . x = H₁(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:

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:
thus ( not x in the carrier of S or X . x c= X . x ) ; :: thesis:

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:
assume x in the carrier' of S ; :: thesis:
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₂(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₂(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₂(x) c= (X * the ResultSort of S) . x & ch . x = H₂(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:

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:
assume x in the carrier of S ; :: thesis:
then X . x = H₁(x) by A1;
hence the Sorts of A . x is Element of X . x by ORDINAL1:8; :: thesis:

end;

then reconsider u = the Sorts of A as ManySortedElement of X ;
take B = UndefMSAlgebra(# X,ch,u #); :: thesis:

hereby :: according to AOFA_A00:def 14,AOFA_A00:def 15 :: thesis:

let o be OperSymbol of S; :: thesis:
let p be FinSequence; :: thesis:
assume A8: p in Args (o,B) ; :: thesis:
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:

A10: now :: thesis:

assume A11: p in Args (o,A) ; :: thesis:
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:

end;

let b be Element of B,(the_result_sort_of o); :: thesis:
assume A13: b = (Den (o,B)) . p ; :: thesis:
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₂(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:

end;

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

hereby :: thesis:

let o be OperSymbol of S; :: thesis:
let a be Element of Args (o,A); :: thesis:
assume Args (o,A) <> {} ; :: thesis:
assume A16: (Den (o,B)) . a <> (Den (o,A)) . a ; :: thesis:
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:

end;

thus the Sorts of B is non-empty ; :: according to MSUALG_1:def 3 :: thesis:
thus verum ; :: thesis: