let MS be non void 1 -element segmental ManySortedSign ; for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
let A be non-empty MSAlgebra over MS; for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
let B be non-empty MSSubAlgebra of A; for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
the charact of (1-Alg B) = Opers ((1-Alg A),S)
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
A1:
the Charact of B = Opers (A,C)
by MSUALG_2:def 9;
set 1B = 1-Alg B;
set 1A = 1-Alg A;
A2:
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #)
by MSUALG_1:def 14;
set f1 = the charact of (1-Alg B);
let S be non empty Subset of (1-Alg A); ( S = the carrier of (1-Alg B) implies the charact of (1-Alg B) = Opers ((1-Alg A),S) )
assume A3:
S = the carrier of (1-Alg B)
; the charact of (1-Alg B) = Opers ((1-Alg A),S)
reconsider f1 = the charact of (1-Alg B) as PFuncFinSequence of S by A3;
A4:
1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #)
by MSUALG_1:def 14;
then A5:
f1 = the Charact of B
by MSUALG_1:def 13;
A6:
C is opers_closed
by MSUALG_2:def 9;
A7:
for n being set
for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds
f1 . n = o /. S
proof
let n be
set ;
for o being operation of (1-Alg A) st n in dom f1 & o = the charact of (1-Alg A) . n holds
f1 . n = o /. Slet o be
operation of
(1-Alg A);
( n in dom f1 & o = the charact of (1-Alg A) . n implies f1 . n = o /. S )
assume that A8:
n in dom f1
and A9:
o = the
charact of
(1-Alg A) . n
;
f1 . n = o /. S
reconsider y =
n as
OperSymbol of
MS by A5, A8, PARTFUN1:def 2;
o =
the
Charact of
A . y
by A2, A9, MSUALG_1:def 13
.=
Den (
y,
A)
by MSUALG_1:def 6
;
then A10:
dom o =
Args (
y,
A)
by FUNCT_2:def 1
.=
(len (the_arity_of y)) -tuples_on (the_sort_of A)
by MSUALG_1:6
;
then A11:
arity o = len (the_arity_of y)
by MARGREL1:def 25;
S is
opers_closed
by A3, Th18;
then A12:
S is_closed_on o
;
A13:
C is_closed_on y
by A6;
A14:
((C #) * the Arity of MS) . y =
Args (
y,
B)
by MSUALG_1:def 4
.=
(arity o) -tuples_on S
by A4, A3, A11, MSUALG_1:6
;
f1 . n =
the
Charact of
B . y
by A4, MSUALG_1:def 13
.=
y /. C
by A1, MSUALG_2:def 8
.=
(Den (y,A)) | (((C #) * the Arity of MS) . y)
by A13, MSUALG_2:def 7
.=
( the Charact of A . y) | (((C #) * the Arity of MS) . y)
by MSUALG_1:def 6
.=
o | ((arity o) -tuples_on S)
by A2, A9, A14, MSUALG_1:def 13
;
hence
f1 . n = o /. S
by A12, UNIALG_2:def 5;
verum
end;
dom f1 =
the carrier' of MS
by A5, PARTFUN1:def 2
.=
dom the Charact of A
by PARTFUN1:def 2
.=
dom the charact of (1-Alg A)
by A2, MSUALG_1:def 13
;
hence
the charact of (1-Alg B) = Opers ((1-Alg A),S)
by A7, UNIALG_2:def 6; verum