let MS be non void 1 -element segmental ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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
let o be operation of (1-Alg A); :: thesis: ( 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 ; :: thesis: 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 ;

now :: thesis: ( ex x being FinSequence st x in dom o & ( for x being FinSequence st x in dom o holds
len (the_arity_of y) = len x ) )

set a = the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A);
the Element of (len (the_arity_of y)) -tuples_on (the_sort_of A) in dom o by A10;
hence ex x being FinSequence st x in dom o ; :: thesis: for x being FinSequence st x in dom o holds
len (the_arity_of y) = len x
let x be FinSequence; :: thesis: ( x in dom o implies len (the_arity_of y) = len x )
assume x in dom o ; :: thesis: len (the_arity_of y) = len x
then ex s being Element of (the_sort_of A) * st
( x = s & len s = len (the_arity_of y) ) by A10;
hence len (the_arity_of y) = len x ; :: thesis: verum

end;

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; :: thesis: 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; :: thesis: verum