let S be non void Signature; for X being V5() ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union A holds
(Sym o,X) -tree p in A . (the_result_sort_of o) )
let X be V5() ManySortedSet of the carrier of S; for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union A holds
(Sym o,X) -tree p in A . (the_result_sort_of o) )
set A = FreeMSA X;
let T be MSSubset of (FreeMSA X); ( T is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union T holds
(Sym o,X) -tree p in T . (the_result_sort_of o) )
hereby ( ( for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union T holds
(Sym o,X) -tree p in T . (the_result_sort_of o) ) implies T is opers_closed )
assume A1:
T is
opers_closed
;
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union T holds
(Sym o,X) -tree p in T . (the_result_sort_of o)let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym o,X st rng p c= Union T holds
(Sym o,X) -tree p in T . (the_result_sort_of o)let p be
ArgumentSeq of
Sym o,
X;
( rng p c= Union T implies (Sym o,X) -tree p in T . (the_result_sort_of o) )
T is_closed_on o
by A1, MSUALG_2:def 7;
then A2:
rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) c= (T * the ResultSort of S) . o
by MSUALG_2:def 6;
A3:
p is
Element of
Args o,
(FreeMSA X)
by INSTALG1:2;
A4:
dom p = dom (the_arity_of o)
by MSATERM:22;
A5:
dom T = the
carrier of
S
by PARTFUN1:def 4;
assume A6:
rng p c= Union T
;
(Sym o,X) -tree p in T . (the_result_sort_of o)A7:
now let x be
set ;
( x in dom (the_arity_of o) implies p . x in (T * (the_arity_of o)) . x )assume A8:
x in dom (the_arity_of o)
;
p . x in (T * (the_arity_of o)) . xthen reconsider i =
x as
Nat ;
reconsider t =
p . i as
Term of
S,
X by A4, A8, MSATERM:22;
A9:
(
the_sort_of t = (the_arity_of o) . x &
(T * (the_arity_of o)) . x = T . ((the_arity_of o) . x) )
by A4, A8, FUNCT_1:23, MSATERM:23;
p . x in rng p
by A4, A8, FUNCT_1:def 5;
then consider y being
set such that A10:
y in dom T
and A11:
p . x in T . y
by A6, CARD_5:10;
T c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 23;
then
T . y c= the
Sorts of
(FreeMSA X) . y
by A5, A10, PBOOLE:def 5;
hence
p . x in (T * (the_arity_of o)) . x
by A5, A10, A11, A9, Th8;
verum end;
rng (the_arity_of o) c= dom T
by A5;
then
dom (T * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
then A12:
p in product (T * (the_arity_of o))
by A4, A7, CARD_3:18;
A13:
((T # ) * the Arity of S) . o =
(T # ) . (the Arity of S . o)
by FUNCT_2:21
.=
(T # ) . (the_arity_of o)
by MSUALG_1:def 6
.=
product (T * (the_arity_of o))
by PBOOLE:def 19
;
then A14:
((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) . p = (Den o,(FreeMSA X)) . p
by A12, FUNCT_1:72;
dom (Den o,(FreeMSA X)) = Args o,
(FreeMSA X)
by FUNCT_2:def 1;
then
p in dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o))
by A13, A3, A12, RELAT_1:86;
then A15:
(Den o,(FreeMSA X)) . p in rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o))
by A14, FUNCT_1:def 5;
(T * the ResultSort of S) . o =
T . (the ResultSort of S . o)
by FUNCT_2:21
.=
T . (the_result_sort_of o)
by MSUALG_1:def 7
;
then
(
[o,the carrier of S] = Sym o,
X &
(Den o,(FreeMSA X)) . p in T . (the_result_sort_of o) )
by A2, A15, MSAFREE:def 11;
hence
(Sym o,X) -tree p in T . (the_result_sort_of o)
by A3, INSTALG1:4;
verum
end;
assume A16:
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,X st rng p c= Union T holds
(Sym o,X) -tree p in T . (the_result_sort_of o)
; T is opers_closed
let o be OperSymbol of S; MSUALG_2:def 7 T is_closed_on o
let x be set ; TARSKI:def 3,MSUALG_2:def 6 ( not x in proj2 ((Den o,(FreeMSA X)) | ((the Arity of S * (T # )) . o)) or x in (the ResultSort of S * T) . o )
A17: (T * the ResultSort of S) . o =
T . (the ResultSort of S . o)
by FUNCT_2:21
.=
T . (the_result_sort_of o)
by MSUALG_1:def 7
;
assume
x in rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o))
; x in (the ResultSort of S * T) . o
then consider y being set such that
A18:
y in dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o))
and
A19:
x = ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) . y
by FUNCT_1:def 5;
reconsider y = y as Element of Args o,(FreeMSA X) by A18;
reconsider p = y as ArgumentSeq of Sym o,X by INSTALG1:2;
A20:
dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) c= ((T # ) * the Arity of S) . o
by RELAT_1:87;
A21: ((T # ) * the Arity of S) . o =
(T # ) . (the Arity of S . o)
by FUNCT_2:21
.=
(T # ) . (the_arity_of o)
by MSUALG_1:def 6
.=
product (T * (the_arity_of o))
by PBOOLE:def 19
;
A22:
rng p c= Union T
proof
let z be
set ;
TARSKI:def 3 ( not z in rng p or z in Union T )
A23:
dom T = the
carrier of
S
by PARTFUN1:def 4;
assume
z in rng p
;
z in Union T
then consider a being
set such that A24:
a in dom p
and A25:
z = p . a
by FUNCT_1:def 5;
A26:
dom p = dom (T * (the_arity_of o))
by A18, A21, A20, CARD_3:18;
then A27:
(
z in (T * (the_arity_of o)) . a &
(T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) )
by A18, A21, A20, A24, A25, CARD_3:18, FUNCT_1:22;
rng (the_arity_of o) c= the
carrier of
S
;
then
dom (T * (the_arity_of o)) = dom (the_arity_of o)
by A23, RELAT_1:46;
then
(the_arity_of o) . a in rng (the_arity_of o)
by A24, A26, FUNCT_1:def 5;
hence
z in Union T
by A23, A27, CARD_5:10;
verum
end;
x =
(Den o,(FreeMSA X)) . y
by A18, A19, FUNCT_1:70
.=
[o,the carrier of S] -tree y
by INSTALG1:4
.=
(Sym o,X) -tree p
by MSAFREE:def 11
;
hence
x in (the ResultSort of S * T) . o
by A16, A17, A22; verum