let S be non void Signature; for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds
( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )
let X, Y be ManySortedSet of the carrier of S; ( X c= Y & X is with_missing_variables implies ( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) ) )
assume that
A1:
X c= Y
and
A2:
X is with_missing_variables
; ( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )
A3:
Y is with_missing_variables
by A1, A2, Th117;
set G = DTConMSA X;
set G9 = DTConMSA Y;
A4:
the carrier of (DTConMSA X) c= the carrier of (DTConMSA Y)
by A1, Th118, XBOOLE_1:9;
A5:
Terminals (DTConMSA X) = Union (coprod X)
by A2, Th120;
A6:
Terminals (DTConMSA Y) = Union (coprod Y)
by A3, Th120;
hence
Terminals (DTConMSA X) c= Terminals (DTConMSA Y)
by A1, A5, Th118; ( the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )
A7:
the carrier of (DTConMSA X) * c= the carrier of (DTConMSA Y) *
by A4, FINSEQ_1:62;
thus
the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y)
TS (DTConMSA X) c= TS (DTConMSA Y)proof
let a,
b be
object ;
RELAT_1:def 3 ( not b ast in the Rules of (DTConMSA X) or b ast in the Rules of (DTConMSA Y) )
assume A8:
[a,b] in the
Rules of
(DTConMSA X)
;
b ast in the Rules of (DTConMSA Y)
then A9:
a in [: the carrier' of S,{ the carrier of S}:]
by MSAFREE1:2;
reconsider a =
a as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by A9, XBOOLE_0:def 3;
reconsider a9 =
a as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod Y)) by A9, XBOOLE_0:def 3;
reconsider b =
b as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, MSAFREE1:2;
reconsider b9 =
b as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod Y))) * by A7;
now for o being OperSymbol of S st [o, the carrier of S] = a9 holds
( len b9 = len (the_arity_of o) & ( for x being set st x in dom b9 holds
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) ) ) )let o be
OperSymbol of
S;
( [o, the carrier of S] = a9 implies ( len b9 = len (the_arity_of o) & ( for x being set st x in dom b9 holds
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) ) ) ) )assume A10:
[o, the carrier of S] = a9
;
( len b9 = len (the_arity_of o) & ( for x being set st x in dom b9 holds
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) ) ) )hence A11:
len b9 = len (the_arity_of o)
by A8, MSAFREE:def 7;
for x being set st x in dom b9 holds
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) )let x be
set ;
( x in dom b9 implies ( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) ) )assume A12:
x in dom b9
;
( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) ) )hence
(
b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x )
by A8, A10, MSAFREE:def 7;
( b9 . x in Union (coprod Y) implies b9 . x in coprod (((the_arity_of o) . x),Y) )A13:
Union (coprod Y) misses [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:4;
A14:
b . x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
by A12, DTCONSTR:2;
A15:
dom b9 = Seg (len b9)
by FINSEQ_1:def 3;
dom (the_arity_of o) = Seg (len b9)
by A11, FINSEQ_1:def 3;
then A16:
(the_arity_of o) . x in the
carrier of
S
by A12, A15, DTCONSTR:2;
assume A17:
b9 . x in Union (coprod Y)
;
b9 . x in coprod (((the_arity_of o) . x),Y)
(
b . x in [: the carrier' of S,{ the carrier of S}:] or
b . x in Union (coprod X) )
by A14, XBOOLE_0:def 3;
then
b . x in coprod (
((the_arity_of o) . x),
X)
by A8, A10, A12, A13, A17, MSAFREE:def 7, XBOOLE_0:3;
then A18:
ex
a being
set st
(
a in X . ((the_arity_of o) . x) &
b . x = [a,((the_arity_of o) . x)] )
by A16, MSAFREE:def 2;
X . ((the_arity_of o) . x) c= Y . ((the_arity_of o) . x)
by A1, A16;
hence
b9 . x in coprod (
((the_arity_of o) . x),
Y)
by A16, A18, MSAFREE:def 2;
verum end;
hence
b ast in the
Rules of
(DTConMSA Y)
by A9, MSAFREE:def 7;
verum
end;
hence
TS (DTConMSA X) c= TS (DTConMSA Y)
by A1, A5, A6, Th116, Th118; verum