A1:
the_charact_of A is quasi_total
proof
let n be
Nat;
:: according to UNIALG_1:def 5 :: 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
let x be
FinSequence of
the_sort_of A;
:: according to UNIALG_1:def 2 :: 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
reconsider o =
n as
OperSymbol of
MS by A2, PARTFUN1:def 4;
A8:
((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 A11:
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 A8, Th11
;
then
len y = len (the_arity_of o)
by A4, A5, FINSEQ_1:def 18;
then
y is
Element of
dom h
by A11, FINSEQ_2:110;
hence
y in dom h
by A5;
:: thesis: verum
end;
A12:
the_charact_of A is homogeneous
proof
let n be
Nat;
:: according to UNIALG_1:def 4 :: 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 A13:
n in dom (the_charact_of A)
and A14:
h = (the_charact_of A) . n
;
:: thesis: h is homogeneous
let x,
y be
FinSequence;
:: according to UNIALG_1:def 1 :: thesis: ( not x in dom h or not y in dom h or len x = len y )
assume A15:
(
x in dom h &
y in dom h )
;
:: thesis: len x = len y
reconsider o =
n as
OperSymbol of
MS by A13, PARTFUN1:def 4;
A18:
((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 A14, PBOOLE:def 18;
then A21:
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 A18, Th11
;
hence len x =
len (the_arity_of o)
by A15, FINSEQ_1:def 18
.=
len y
by A15, A21, FINSEQ_1:def 18
;
:: thesis: verum
end;
the_charact_of A is non-empty
hence
UAStr(# (the_sort_of A),(the_charact_of A) #) is strict non-empty Universal_Algebra
by A1, A12, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum