let S be non empty non void ManySortedSign ; :: thesis: for s, s1 being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for C being context of x st X is non-trivial & the_sort_of C = s1 holds
for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let s, s1 be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for C being context of x st X is non-trivial & the_sort_of C = s1 holds
for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for C being context of x st X is non-trivial & the_sort_of C = s1 holds
for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let x be Element of X . s; :: thesis: for C being context of x st X is non-trivial & the_sort_of C = s1 holds
for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let C be context of x; :: thesis: ( X is non-trivial & the_sort_of C = s1 implies for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t) )
assume ZZ: X is non-trivial ; :: thesis: ( not the_sort_of C = s1 or for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t) )
assume Z0: the_sort_of C = s1 ; :: thesis: for x1 being Element of X . s1
for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let x1 be Element of X . s1; :: thesis: for C1 being context of x1
for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let C1 be context of x1; :: thesis: for C2 being context of x st C2 = C1 -sub C holds
for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let C2 be context of x; :: thesis: ( C2 = C1 -sub C implies for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t) )
assume Z1: C2 = C1 -sub C ; :: thesis: for t being Element of (Free (S,X)) st the_sort_of t = s holds
C2 -sub t = C1 -sub (C -sub t)
let t be Element of (Free (S,X)); :: thesis: ( the_sort_of t = s implies C2 -sub t = C1 -sub (C -sub t) )
assume Z2: the_sort_of t = s ; :: thesis: C2 -sub t = C1 -sub (C -sub t)
A0: the_sort_of (C -sub t) = s1 by Z0, SORT;
defpred S1[ context of x1] means for C1 being context of x1
for C2 being context of x st C1 = $1 & C2 = C1 -sub C holds
C2 -sub t = C1 -sub (C -sub t);
A1: S1[x1 -term ]
proof
let C1 be context of x1; :: thesis: for C2 being context of x st C1 = x1 -term & C2 = C1 -sub C holds
C2 -sub t = C1 -sub (C -sub t)
let C2 be context of x; :: thesis: ( C1 = x1 -term & C2 = C1 -sub C implies C2 -sub t = C1 -sub (C -sub t) )
assume B1: ( C1 = x1 -term & C2 = C1 -sub C ) ; :: thesis: C2 -sub t = C1 -sub (C -sub t)
then C2 = C by Z0, Th41;
hence C2 -sub t = C1 -sub (C -sub t) by B1, A0, Th41; :: thesis: verum
end;
A2: for o being OperSymbol of S
for w being Element of Args (o,(Free (S,X))) st w is x1 -context_including & S1[x1 -context_in w] holds
for C being context of x1 st C = o -term w holds
S1[C]
proof
let o be OperSymbol of S; :: thesis: for w being Element of Args (o,(Free (S,X))) st w is x1 -context_including & S1[x1 -context_in w] holds
for C being context of x1 st C = o -term w holds
S1[C]
let w be Element of Args (o,(Free (S,X))); :: thesis: ( w is x1 -context_including & S1[x1 -context_in w] implies for C being context of x1 st C = o -term w holds
S1[C] )
assume Z3: w is x1 -context_including ; :: thesis: ( not S1[x1 -context_in w] or for C being context of x1 st C = o -term w holds
S1[C] )
assume Z4: S1[x1 -context_in w] ; :: thesis: for C being context of x1 st C = o -term w holds
S1[C]
let C1 be context of x1; :: thesis: ( C1 = o -term w implies S1[C1] )
assume Z5: C1 = o -term w ; :: thesis: S1[C1]
let CC be context of x1; :: thesis: for C2 being context of x st CC = C1 & C2 = CC -sub C holds
C2 -sub t = CC -sub (C -sub t)
let C2 be context of x; :: thesis: ( CC = C1 & C2 = CC -sub C implies C2 -sub t = CC -sub (C -sub t) )
assume B2: ( CC = C1 & C2 = CC -sub C ) ; :: thesis: C2 -sub t = CC -sub (C -sub t)
set i = x1 -context_pos_in w;
B3: ( x1 -context_pos_in w in dom w & dom w = dom (the_arity_of o) & x1 -context_in w = w . (x1 -context_pos_in w) ) by Z3, Th71, MSUALG_3:6;
then x1 -context_in w in the Sorts of (Free (S,X)) . ((the_arity_of o) /. (x1 -context_pos_in w)) by MSUALG_6:2;
then B7: the_sort_of (x1 -context_in w) = (the_arity_of o) /. (x1 -context_pos_in w) by SORT;
then reconsider p = w +* ((x1 -context_pos_in w),((x1 -context_in w) -sub (C -sub t))), q = w +* ((x1 -context_pos_in w),((x1 -context_in w) -sub C)) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
B5: ( C2 = o -term q & C1 -sub (C -sub t) = o -term p ) by ZZ, A0, Z0, Z3, Z5, B2, Th43;
then B6: ( q is x -context_including & dom q = dom (the_arity_of o) ) by Th53, MSUALG_3:6;
reconsider A = Coim (((x1 -context_in w) -sub C),[x,s]) as finite set ;
( Segm 1 = Segm (card (Coim (C,[x,s]))) & Segm (card (Coim (C,[x,s]))) = card (Coim (C,[x,s])) & card (Coim (C,[x,s])) c= card (Coim (((x1 -context_in w) -sub C),[x,s])) & card (Coim (((x1 -context_in w) -sub C),[x,s])) = Segm (card (Coim (((x1 -context_in w) -sub C),[x,s]))) ) by ZZ, Z0, Th70, CONTEXT;
then B9: ( not (x1 -context_in w) -sub C is x -omitting & q /. (x1 -context_pos_in w) = q . (x1 -context_pos_in w) & q . (x1 -context_pos_in w) = (x1 -context_in w) -sub C ) by B3, B6, PARTFUN1:def 6, FUNCT_7:31;
then reconsider C3 = (x1 -context_in w) -sub C as context of x by B3, B6;
the_sort_of C3 = (the_arity_of o) /. (x1 -context_pos_in w) by B7, SORT;
then reconsider u = w +* ((x1 -context_pos_in w),(C3 -sub t)) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
C3 in rng q by B9, B6, B3, FUNCT_1:def 3;
then ( o -term p = o -term u & x -context_pos_in q = x1 -context_pos_in w & q +* ((x1 -context_pos_in w),(C3 -sub t)) = u & x -context_in q = C3 ) by B6, Z4, B9, CIn, CPI, FUNCT_7:34;
hence C2 -sub t = CC -sub (C -sub t) by B2, ZZ, Th43, Z2, B5, Th53; :: thesis: verum
end;
S1[C1] from MSAFREE5:sch 4(A1, A2);
hence C2 -sub t = C1 -sub (C -sub t) by Z1; :: thesis: verum