let S be non void Signature; :: thesis: for X being V8() 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 V8() ManySortedSet of the carrier of S; :: thesis: 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); :: thesis: ( 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) )

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) ; :: thesis: T is opers_closed

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: T is_closed_on o

let x be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis: ( 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:15

.= T . (the_result_sort_of o) by MSUALG_1:def 2 ;

assume x in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) ; :: thesis: x in ( the ResultSort of S * T) . o

then consider y being object 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 3;

y in dom (Den (o,(FreeMSA X))) by A18, RELAT_1:57;

then reconsider y = y as Element of Args (o,(FreeMSA X)) ;

reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1;

A20: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15

.= (T #) . (the_arity_of o) by MSUALG_1:def 1

.= product (T * (the_arity_of o)) by FINSEQ_2:def 5 ;

A21: rng p c= Union T

.= [o, the carrier of S] -tree y by INSTALG1:3

.= (Sym (o,X)) -tree p by MSAFREE:def 9 ;

hence x in ( the ResultSort of S * T) . o by A16, A17, A21; :: thesis: verum

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 V8() ManySortedSet of the carrier of S; :: thesis: 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); :: thesis: ( 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 :: thesis: ( ( 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 A16:
for o being OperSymbol of Sfor 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
; :: thesis: 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; :: thesis: 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); :: thesis: ( 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;

then A2: rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o ;

A3: p is Element of Args (o,(FreeMSA X)) by INSTALG1:1;

A4: dom p = dom (the_arity_of o) by MSATERM:22;

A5: dom T = the carrier of S by PARTFUN1:def 2;

assume A6: rng p c= Union T ; :: thesis: (Sym (o,X)) -tree p in T . (the_result_sort_of o)

then dom (T * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

then A12: p in product (T * (the_arity_of o)) by A4, A7, CARD_3:9;

A13: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15

.= (T #) . (the_arity_of o) by MSUALG_1:def 1

.= product (T * (the_arity_of o)) by FINSEQ_2:def 5 ;

then A14: ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . p = (Den (o,(FreeMSA X))) . p by A12, FUNCT_1:49;

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:57;

then A15: (Den (o,(FreeMSA X))) . p in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A14, FUNCT_1:def 3;

(T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15

.= T . (the_result_sort_of o) by MSUALG_1:def 2 ;

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 9;

hence (Sym (o,X)) -tree p in T . (the_result_sort_of o) by A3, INSTALG1:3; :: thesis: verum

end;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; :: thesis: 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); :: thesis: ( 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;

then A2: rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o ;

A3: p is Element of Args (o,(FreeMSA X)) by INSTALG1:1;

A4: dom p = dom (the_arity_of o) by MSATERM:22;

A5: dom T = the carrier of S by PARTFUN1:def 2;

assume A6: rng p c= Union T ; :: thesis: (Sym (o,X)) -tree p in T . (the_result_sort_of o)

A7: now :: thesis: for x being object st x in dom (the_arity_of o) holds

p . x in (T * (the_arity_of o)) . x

rng (the_arity_of o) c= dom T
by A5;p . x in (T * (the_arity_of o)) . x

let x be object ; :: thesis: ( 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) ; :: thesis: p . x in (T * (the_arity_of o)) . x

then 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:13, MSATERM:23;

p . x in rng p by A4, A8, FUNCT_1:def 3;

then consider y being object such that

A10: y in dom T and

A11: p . x in T . y by A6, CARD_5:2;

T c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then T . y c= the Sorts of (FreeMSA X) . y by A10;

hence p . x in (T * (the_arity_of o)) . x by A10, A11, A9, Th7; :: thesis: verum

end;assume A8: x in dom (the_arity_of o) ; :: thesis: p . x in (T * (the_arity_of o)) . x

then 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:13, MSATERM:23;

p . x in rng p by A4, A8, FUNCT_1:def 3;

then consider y being object such that

A10: y in dom T and

A11: p . x in T . y by A6, CARD_5:2;

T c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then T . y c= the Sorts of (FreeMSA X) . y by A10;

hence p . x in (T * (the_arity_of o)) . x by A10, A11, A9, Th7; :: thesis: verum

then dom (T * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

then A12: p in product (T * (the_arity_of o)) by A4, A7, CARD_3:9;

A13: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15

.= (T #) . (the_arity_of o) by MSUALG_1:def 1

.= product (T * (the_arity_of o)) by FINSEQ_2:def 5 ;

then A14: ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . p = (Den (o,(FreeMSA X))) . p by A12, FUNCT_1:49;

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:57;

then A15: (Den (o,(FreeMSA X))) . p in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A14, FUNCT_1:def 3;

(T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15

.= T . (the_result_sort_of o) by MSUALG_1:def 2 ;

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 9;

hence (Sym (o,X)) -tree p in T . (the_result_sort_of o) by A3, INSTALG1:3; :: thesis: verum

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) ; :: thesis: T is opers_closed

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: T is_closed_on o

let x be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis: ( 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:15

.= T . (the_result_sort_of o) by MSUALG_1:def 2 ;

assume x in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) ; :: thesis: x in ( the ResultSort of S * T) . o

then consider y being object 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 3;

y in dom (Den (o,(FreeMSA X))) by A18, RELAT_1:57;

then reconsider y = y as Element of Args (o,(FreeMSA X)) ;

reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1;

A20: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15

.= (T #) . (the_arity_of o) by MSUALG_1:def 1

.= product (T * (the_arity_of o)) by FINSEQ_2:def 5 ;

A21: rng p c= Union T

proof

x =
(Den (o,(FreeMSA X))) . y
by A18, A19, FUNCT_1:47
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in Union T )

A22: dom T = the carrier of S by PARTFUN1:def 2;

assume z in rng p ; :: thesis: z in Union T

then consider a being object such that

A23: a in dom p and

A24: z = p . a by FUNCT_1:def 3;

A25: dom p = dom (T * (the_arity_of o)) by A18, A20, CARD_3:9;

then A26: ( z in (T * (the_arity_of o)) . a & (T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) ) by A18, A20, A23, A24, CARD_3:9, FUNCT_1:12;

rng (the_arity_of o) c= the carrier of S ;

then dom (T * (the_arity_of o)) = dom (the_arity_of o) by A22, RELAT_1:27;

then (the_arity_of o) . a in rng (the_arity_of o) by A23, A25, FUNCT_1:def 3;

hence z in Union T by A22, A26, CARD_5:2; :: thesis: verum

end;A22: dom T = the carrier of S by PARTFUN1:def 2;

assume z in rng p ; :: thesis: z in Union T

then consider a being object such that

A23: a in dom p and

A24: z = p . a by FUNCT_1:def 3;

A25: dom p = dom (T * (the_arity_of o)) by A18, A20, CARD_3:9;

then A26: ( z in (T * (the_arity_of o)) . a & (T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) ) by A18, A20, A23, A24, CARD_3:9, FUNCT_1:12;

rng (the_arity_of o) c= the carrier of S ;

then dom (T * (the_arity_of o)) = dom (the_arity_of o) by A22, RELAT_1:27;

then (the_arity_of o) . a in rng (the_arity_of o) by A23, A25, FUNCT_1:def 3;

hence z in Union T by A22, A26, CARD_5:2; :: thesis: verum

.= [o, the carrier of S] -tree y by INSTALG1:3

.= (Sym (o,X)) -tree p by MSAFREE:def 9 ;

hence x in ( the ResultSort of S * T) . o by A16, A17, A21; :: thesis: verum