A1: the_charact_of A is quasi_total
proof
let n be Nat; :: according to MARGREL1:def 24 :: thesis: for b1 being Element of K10(K11(((the_sort_of A) *),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b1 = (the_charact_of A) . n or b1 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 2;
let x be FinSequence of the_sort_of A; :: according to MARGREL1:def 22 :: thesis: for b1 being FinSequence of the_sort_of A holds
( not len x = len b1 or not x in dom h or b1 in dom h )
let y be FinSequence of the_sort_of A; :: thesis: ( not len x = len y or not x in dom h or y in dom h )
assume that
A4: len x = len y and
A5: x in dom h ; :: thesis: y in dom 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 15;
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, Th6 ;
then len y = len (the_arity_of o) by A4, A5, CARD_1:def 7;
then y is Element of dom h by A7, FINSEQ_2:92;
hence y in dom h by A5; :: thesis: verum
end;
A8: the_charact_of A is homogeneous
proof
let n be Nat; :: according to MARGREL1:def 23 :: thesis: for b1 being Element of K10(K11(((the_sort_of A) *),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b1 = (the_charact_of A) . n or b1 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 2;
thus dom h is with_common_domain :: according to MARGREL1:def 21 :: 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 15;
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, Th6 ;
hence len x = len (the_arity_of o) by A11, CARD_1:def 7
.= len y by A12, A14, CARD_1:def 7 ;
:: thesis: verum
end;
end;
the_charact_of A is non-empty
proof
let n be object ; :: according to FUNCT_1:def 9 :: thesis: ( not n in dom (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 2;
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 Universal_Algebra by A1, A8, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; :: thesis: verum