A1: the_charact_of A is quasi_total

proof

let n be Nat; :: according to MARGREL1:def 25 :: thesis: for b₁ being Element of K10(K11(((the_sort_of A) * ),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b₁ = (the_charact_of A) . n or b₁ is quasi_total )
let h be PartFunc of ((the_sort_of A) * ),(the_sort_of A); :: thesis: ( not n in dom (the_charact_of A) or not h = (the_charact_of A) . n or h is quasi_total )
assume that
A2: n in dom (the_charact_of A) and
A3: h = (the_charact_of A) . n ; :: thesis: h is quasi_total
reconsider o = n as OperSymbol of MS by A2, PARTFUN1:def 4;
let x be FinSequence of the_sort_of A; :: according to MARGREL1:def 23 :: thesis: for b₁ being FinSequence of the_sort_of A holds
( not len x = len b₁ or not x in proj1 h or b₁ in proj1 h )
let y be FinSequence of the_sort_of A; :: thesis: ( not len x = len y or not x in proj1 h or y in proj1 h )
assume that
A4: len x = len y and
A5: x in dom h ; :: thesis: y in proj1 h
A6: ((the Sorts of A # ) * the Arity of MS) . o = Args o,A ;
h is Function of (((the Sorts of A # ) * the Arity of MS) . o),((the Sorts of A * the ResultSort of MS) . o) by A3, PBOOLE:def 18;
then A7: dom h = ((the Sorts of A # ) * the Arity of MS) . o by FUNCT_2:def 1
.= (len (the_arity_of o)) -tuples_on (the_sort_of A) by A6, Th11 ;
then len y = len (the_arity_of o) by A4, A5, FINSEQ_1:def 18;
then y is Element of dom h by A7, FINSEQ_2:110;
hence y in proj1 h by A5; :: thesis: verum

end;

A8: the_charact_of A is homogeneous

proof

let n be Nat; :: according to MARGREL1:def 24 :: thesis: for b₁ being Element of K10(K11(((the_sort_of A) * ),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b₁ = (the_charact_of A) . n or b₁ is homogeneous )
let h be PartFunc of ((the_sort_of A) * ),(the_sort_of A); :: thesis: ( not n in dom (the_charact_of A) or not h = (the_charact_of A) . n or h is homogeneous )
assume that
A9: n in dom (the_charact_of A) and
A10: h = (the_charact_of A) . n ; :: thesis: h is homogeneous
reconsider o = n as OperSymbol of MS by A9, PARTFUN1:def 4;
thus dom h is with_common_domain :: according to MARGREL1:def 22 :: thesis: verum

proof

let x, y be FinSequence; :: according to MARGREL1:def 1 :: thesis: ( not x in dom h or not y in dom h or len x = len y )
assume that
A11: x in dom h and
A12: y in dom h ; :: thesis: len x = len y
A13: ((the Sorts of A # ) * the Arity of MS) . o = Args o,A ;
h is Function of (((the Sorts of A # ) * the Arity of MS) . o),((the Sorts of A * the ResultSort of MS) . o) by A10, PBOOLE:def 18;
then A14: dom h = ((the Sorts of A # ) * the Arity of MS) . o by FUNCT_2:def 1
.= (len (the_arity_of o)) -tuples_on (the_sort_of A) by A13, Th11 ;
hence len x = len (the_arity_of o) by A11, FINSEQ_1:def 18
.= len y by A12, A14, FINSEQ_1:def 18 ;
:: thesis: verum

end;

end;

the_charact_of A is non-empty

proof

let n be set ; :: according to FUNCT_1:def 15 :: thesis: ( not n in proj1 (the_charact_of A) or not (the_charact_of A) . n is empty )
assume n in dom (the_charact_of A) ; :: thesis: not (the_charact_of A) . n is empty
then reconsider o = n as OperSymbol of MS by PARTFUN1:def 4;
set h = (the_charact_of A) . n;
(the_charact_of A) . n = Den o,A ;
hence not (the_charact_of A) . n is empty ; :: thesis: verum

end;

hence UAStr(# (the_sort_of A),(the_charact_of A) #) is strict non-empty Universal_Algebra by A1, A8, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum