let U0 be Universal_Algebra; for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra
let A be non empty Subset of U0; UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra
set C = UAStr(# A,(Opers (U0,A)) #);
A1:
dom the charact of UAStr(# A,(Opers (U0,A)) #) = dom the charact of U0
by Def6;
for n being object st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) holds
not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty
proof
let n be
object ;
( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) implies not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty )
assume A2:
n in dom the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
;
not the charact of UAStr(# A,(Opers (U0,A)) #) . n is empty
then reconsider o = the
charact of
U0 . n as
operation of
U0 by A1, FUNCT_1:def 3;
the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
. n = o /. A
by A2, Def6;
hence
not the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
. n is
empty
;
verum
end;
then A3:
the charact of UAStr(# A,(Opers (U0,A)) #) is non-empty
by FUNCT_1:def 9;
for n being Nat
for h being PartFunc of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds
h is quasi_total
proof
let n be
Nat;
for h being PartFunc of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds
h is quasi_total let h be
PartFunc of
( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the
carrier of
UAStr(#
A,
(Opers (U0,A)) #);
( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n implies h is quasi_total )
assume that A4:
n in dom the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
and A5:
h = the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
. n
;
h is quasi_total
reconsider o = the
charact of
U0 . n as
operation of
U0 by A1, A4, FUNCT_1:def 3;
h = o /. A
by A4, A5, Def6;
hence
h is
quasi_total
;
verum
end;
then A6:
the charact of UAStr(# A,(Opers (U0,A)) #) is quasi_total
;
for n being Nat
for h being PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds
h is homogeneous
proof
let n be
Nat;
for h being PartFunc of ( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the carrier of UAStr(# A,(Opers (U0,A)) #) st n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n holds
h is homogeneous let h be
PartFunc of
( the carrier of UAStr(# A,(Opers (U0,A)) #) *), the
carrier of
UAStr(#
A,
(Opers (U0,A)) #);
( n in dom the charact of UAStr(# A,(Opers (U0,A)) #) & h = the charact of UAStr(# A,(Opers (U0,A)) #) . n implies h is homogeneous )
assume that A7:
n in dom the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
and A8:
h = the
charact of
UAStr(#
A,
(Opers (U0,A)) #)
. n
;
h is homogeneous
reconsider o = the
charact of
U0 . n as
operation of
U0 by A1, A7, FUNCT_1:def 3;
h = o /. A
by A7, A8, Def6;
hence
h is
homogeneous
;
verum
end;
then A9:
the charact of UAStr(# A,(Opers (U0,A)) #) is homogeneous
;
the charact of UAStr(# A,(Opers (U0,A)) #) <> {}
by A1, RELAT_1:38, RELAT_1:41;
hence
UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra
by A9, A6, A3, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; verum