let a be object ; :: thesis: for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let s be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X))
for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let t be Element of (Free (S,X)); :: thesis: for C being context of x st X is non-trivial & the_sort_of t = s holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a))
let C be context of x; :: thesis: ( X is non-trivial & the_sort_of t = s implies card (Coim (t,a)) c= card (Coim ((C -sub t),a)) )
assume that
ZZ: X is non-trivial and
Z0: the_sort_of t = s ; :: thesis: card (Coim (t,a)) c= card (Coim ((C -sub t),a))
defpred S₁[ context of x] means for C being context of x st C = $1 holds
card (Coim (t,a)) c= card (Coim ((C -sub t),a));
A0: S₁[x -term ] by Z0, Th41;
A1: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S₁[x -context_in p] holds
for C being context of x st C = o -term p holds
S₁[C]

proof

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S₁[x -context_in p] holds
for C being context of x st C = o -term p holds
S₁[C]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including & S₁[x -context_in p] implies for C being context of x st C = o -term p holds
S₁[C] )
assume Z1: p is x -context_including ; :: thesis: ( not S₁[x -context_in p] or for C being context of x st C = o -term p holds
S₁[C] )
assume Z2: S₁[x -context_in p] ; :: thesis: for C being context of x st C = o -term p holds
S₁[C]
set i = x -context_pos_in p;
A6: ( x -context_pos_in p in dom p & dom p = dom (the_arity_of o) ) by Z1, Th71, MSUALG_3:6;
then consider j being Nat such that
A3: x -context_pos_in p = 1 + j by NAT_1:10, FINSEQ_3:25;
card (<*j*> ^^ (Coim (((x -context_in p) -sub t),a))) = card (Coim (((x -context_in p) -sub t),a)) by Th1;
then consider f being Function such that
A2: ( f is one-to-one & dom f = Coim (t,a) & rng f c= <*j*> ^^ (Coim (((x -context_in p) -sub t),a)) ) by Z2, CARD_1:10;
let C be context of x; :: thesis: ( C = o -term p implies S₁[C] )
assume Z3: C = o -term p ; :: thesis: S₁[C]
x -context_in p = p . (x -context_pos_in p) by Z1, Th71;
then x -context_in p in the Sorts of (Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) by A6, MSUALG_6:2;
then the_sort_of (x -context_in p) = (the_arity_of o) /. (x -context_pos_in p) by SORT;
then reconsider q = p +* ((x -context_pos_in p),((x -context_in p) -sub t)) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
A4: C -sub t = o -term q by ZZ, Z0, Z1, Z3, Th43;
<*j*> ^^ (Coim (((x -context_in p) -sub t),a)) c= Coim ((C -sub t),a)

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in <*j*> ^^ (Coim (((x -context_in p) -sub t),a)) or r in Coim ((C -sub t),a) )
assume r in <*j*> ^^ (Coim (((x -context_in p) -sub t),a)) ; :: thesis: r in Coim ((C -sub t),a)
then consider n being Element of Coim (((x -context_in p) -sub t),a) such that
A5: ( r = <*j*> ^ n & n in Coim (((x -context_in p) -sub t),a) ) ;
Coim (((x -context_in p) -sub t),a) c= dom ((x -context_in p) -sub t) by RELAT_1:132;
then reconsider n = n as Element of dom ((x -context_in p) -sub t) by A5;
( x -context_pos_in p <= len p & dom q = dom (the_arity_of o) ) by A6, FINSEQ_3:25, MSUALG_3:6;
then ( j < len p & len p = len q & q . (x -context_pos_in p) = (x -context_in p) -sub t ) by A3, Z1, Th71, MSUALG_3:6, NAT_1:13, FINSEQ_3:29, FUNCT_7:31;
then A9: ( <*j*> ^ n in dom (C -sub t) & (C -sub t) . r = ((x -context_in p) -sub t) . n & ((x -context_in p) -sub t) . n in {a} ) by A3, A4, A5, TREES_4:11, TREES_4:12, FUNCT_1:def 7;
thus r in Coim ((C -sub t),a) by A5, A9, FUNCT_1:def 7; :: thesis: verum

end;

then rng f c= Coim ((C -sub t),a) by A2;
hence S₁[C] by A2, CARD_1:10; :: thesis: verum

end;

S₁[C] from MSAFREE5:sch 4(A0, A1);
hence card (Coim (t,a)) c= card (Coim ((C -sub t),a)) ; :: thesis: verum