let S be non void Signature; :: thesis: for X, Y being ManySortedSet of 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 ; :: thesis: ( 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
Z0:
X c= Y
and
Z1:
X is with_missing_variables
; :: thesis: ( 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) )
Z2:
Y is with_missing_variables
by Z0, Z1, LemX;
set G = DTConMSA X;
set G' = DTConMSA Y;
A1:
the carrier of (DTConMSA X) c= the carrier of (DTConMSA Y)
by Z0, LemY0, XBOOLE_1:9;
( Terminals (DTConMSA X) = Union (coprod X) & Terminals (DTConMSA Y) = Union (coprod Y) )
by Z1, Z2, ThTNT;
hence A2:
Terminals (DTConMSA X) c= Terminals (DTConMSA Y)
by Z0, LemY0; :: thesis: ( the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )
A3:
the carrier of (DTConMSA X) * c= the carrier of (DTConMSA Y) *
by A1, FINSEQ_1:83;
thus
the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y)
:: thesis: TS (DTConMSA X) c= TS (DTConMSA Y)proof
let a,
b be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not b ast in the Rules of (DTConMSA X) or b ast in the Rules of (DTConMSA Y) )
assume C1:
[a,b] in the
Rules of
(DTConMSA X)
;
:: thesis: b ast in the Rules of (DTConMSA Y)
then C2:
(
a in [:the carrier' of S,{the carrier of S}:] &
b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * )
by MSAFREE1:2;
then consider a1,
a2 being
set such that C3:
(
a1 in the
carrier' of
S &
a2 in {the carrier of S} &
a = [a1,a2] )
by ZFMISC_1:def 2;
reconsider a1 =
a1 as
OperSymbol of
S by C3;
reconsider a =
a as
Element of
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by C2, XBOOLE_0:def 3;
reconsider a' =
a as
Element of
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod Y)) by C2, XBOOLE_0:def 3;
reconsider b =
b as
Element of
([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by C2;
reconsider b' =
b as
Element of
([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod Y))) * by C2, A3;
now let o be
OperSymbol of
S;
:: thesis: ( [o,the carrier of S] = a' implies ( len b' = len (the_arity_of o) & ( for x being set st x in dom b' holds
( ( b' . 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 ) & ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y ) ) ) ) )assume C4:
[o,the carrier of S] = a'
;
:: thesis: ( len b' = len (the_arity_of o) & ( for x being set st x in dom b' holds
( ( b' . 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 ) & ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y ) ) ) )hence CC:
len b' = len (the_arity_of o)
by C1, MSAFREE:def 9;
:: thesis: for x being set st x in dom b' holds
( ( b' . 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 ) & ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y ) )let x be
set ;
:: thesis: ( x in dom b' implies ( ( b' . 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 ) & ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y ) ) )assume C5:
x in dom b'
;
:: thesis: ( ( b' . 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 ) & ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y ) )hence
(
b' . 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 C1, C4, MSAFREE:def 9;
:: thesis: ( b' . x in Union (coprod Y) implies b' . x in coprod ((the_arity_of o) . x),Y )C6:
(
Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] &
Union (coprod Y) misses [:the carrier' of S,{the carrier of S}:] )
by MSAFREE:4;
C7:
b . x in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))
by C5, DTCONSTR:2;
(
dom b' = Seg (len b') &
dom (the_arity_of o) = Seg (len b') )
by CC, FINSEQ_1:def 3;
then C9:
(the_arity_of o) . x in the
carrier of
S
by C5, DTCONSTR:2;
assume
b' . x in Union (coprod Y)
;
:: thesis: b' . x in coprod ((the_arity_of o) . x),Ythen
( (
b . x in [:the carrier' of S,{the carrier of S}:] or
b . x in Union (coprod X) ) &
b . x nin [:the carrier' of S,{the carrier of S}:] )
by C6, C7, XBOOLE_0:3, XBOOLE_0:def 3;
then
b . x in coprod ((the_arity_of o) . x),
X
by C1, C4, C5, MSAFREE:def 9;
then consider a being
set such that C8:
(
a in X . ((the_arity_of o) . x) &
b . x = [a,((the_arity_of o) . x)] )
by C9, MSAFREE:def 2;
X . ((the_arity_of o) . x) c= Y . ((the_arity_of o) . x)
by Z0, C9, PBOOLE:def 5;
hence
b' . x in coprod ((the_arity_of o) . x),
Y
by C8, C9, MSAFREE:def 2;
:: thesis: verum end;
hence
b ast in the
Rules of
(DTConMSA Y)
by C2, MSAFREE:def 9;
:: thesis: verum
end;
hence
TS (DTConMSA X) c= TS (DTConMSA Y)
by A2, LemTS0; :: thesis: verum