let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for R being b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let s be SortSymbol of S; for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for R being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let Z be non-trivial ManySortedSet of the carrier of S; for z being Element of Z . s
for R being Z,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let z be Element of Z . s; for R being Z,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let R be Z,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let C9 be context of z; for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
let t be Element of (Free (S,Z)); ( the_sort_of t = s implies (canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t))) )
assume A1:
the_sort_of t = s
; (canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))
set H = canonical_homomorphism R;
defpred S1[ context of z] means (canonical_homomorphism R) . ($1 -sub t) = (canonical_homomorphism R) . ($1 -sub (@ ((canonical_homomorphism R) . t)));
B1: the_sort_of (@ ((canonical_homomorphism R) . t)) =
the_sort_of ((canonical_homomorphism R) . t)
by Lem00
.=
the_sort_of t
by Lem0
;
B3: the_sort_of ((z -term) -sub (@ ((canonical_homomorphism R) . t))) =
the_sort_of (z -term)
by SORT
.=
s
by SORT
;
A2:
S1[z -term ]
proof
B5:
(
dom ((canonical_homomorphism R) ** (canonical_homomorphism R)) = (dom (canonical_homomorphism R)) /\ (dom (canonical_homomorphism R)) &
(dom (canonical_homomorphism R)) /\ (dom (canonical_homomorphism R)) = dom (canonical_homomorphism R) &
dom (canonical_homomorphism R) = the
carrier of
S )
by PARTFUN1:def 2, PBOOLE:def 19;
B6:
(
t in the
Sorts of
(Free (S,Z)) . s & the
Sorts of
R . s <> {} &
(canonical_homomorphism R) . s is
Function of
( the Sorts of (Free (S,Z)) . s),
( the Sorts of R . s) )
by A1, SORT;
B4:
(
(z -term) -sub t = t &
(z -term) -sub (@ ((canonical_homomorphism R) . t)) = (canonical_homomorphism R) . t &
(canonical_homomorphism R) . t = ((canonical_homomorphism R) . s) . t )
by A1, B1, Th41, ABBR;
hence (canonical_homomorphism R) . ((z -term) -sub t) =
(((canonical_homomorphism R) ** (canonical_homomorphism R)) . s) . t
by MSAFREE4:48
.=
(((canonical_homomorphism R) . s) * ((canonical_homomorphism R) . s)) . t
by B5, PBOOLE:def 19
.=
((canonical_homomorphism R) . s) . ((z -term) -sub (@ ((canonical_homomorphism R) . t)))
by B4, B6, FUNCT_2:15
.=
(canonical_homomorphism R) . ((z -term) -sub (@ ((canonical_homomorphism R) . t)))
by B3, ABBR
;
verum
end;
A3:
now for o being OperSymbol of S
for p being Element of Args (o,(Free (S,Z))) st p is z -context_including & S1[z -context_in p] holds
for C being context of z st C = o -term p holds
S1[C]let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,Z))) st p is z -context_including & S1[z -context_in p] holds
for C being context of z st C = o -term p holds
S1[C]let p be
Element of
Args (
o,
(Free (S,Z)));
( p is z -context_including & S1[z -context_in p] implies for C being context of z st C = o -term p holds
S1[C] )assume A4:
p is
z -context_including
;
( S1[z -context_in p] implies for C being context of z st C = o -term p holds
S1[C] )assume A5:
S1[
z -context_in p]
;
for C being context of z st C = o -term p holds
S1[C]let C be
context of
z;
( C = o -term p implies S1[C] )assume A6:
C = o -term p
;
S1[C]C2:
(
the_sort_of ((z -context_in p) -sub t) = the_sort_of (z -context_in p) &
the_sort_of (z -context_in p) = (the_arity_of o) . (z -context_pos_in p) )
by A4, Th46, SORT;
then reconsider w =
p +* (
(z -context_pos_in p),
((z -context_in p) -sub t)) as
Element of
Args (
o,
(Free (S,Z)))
by A4, Th42;
Args (
o,
R)
c= Args (
o,
(Free (S,Z)))
by MSAFREE4:41;
then reconsider q =
(canonical_homomorphism R) # w,
r =
(canonical_homomorphism R) # p as
Element of
Args (
o,
(Free (S,Z))) ;
C1:
the_sort_of (@ ((canonical_homomorphism R) . t)) =
the_sort_of ((canonical_homomorphism R) . t)
by Lem00
.=
s
by A1, Lem0
;
C3:
the_sort_of ((z -context_in p) -sub (@ ((canonical_homomorphism R) . t))) = the_sort_of (z -context_in p)
by SORT;
reconsider m =
p +* (
(z -context_pos_in p),
((z -context_in p) -sub (@ ((canonical_homomorphism R) . t)))) as
Element of
Args (
o,
(Free (S,Z)))
by A4, C2, C3, Th42;
A9:
q =
r +* (
(z -context_pos_in p),
((canonical_homomorphism R) . ((z -context_in p) -sub (@ ((canonical_homomorphism R) . t)))))
by A5, A4, Th71, Th47
.=
(canonical_homomorphism R) # m
by A4, Th71, Th47
;
C -sub t = o -term w
by A1, A4, A6, Th43;
then (canonical_homomorphism R) . (C -sub t) =
((canonical_homomorphism R) . (the_sort_of (o -term w))) . (o -term w)
by ABBR
.=
((canonical_homomorphism R) . (the_result_sort_of o)) . (o -term w)
by Th8
.=
((canonical_homomorphism R) . (the_result_sort_of o)) . ((Den (o,(Free (S,Z)))) . w)
by MSAFREE4:13
.=
(Den (o,R)) . ((canonical_homomorphism R) # w)
by MSAFREE4:def 10, MSUALG_3:def 7
.=
((canonical_homomorphism R) . (the_result_sort_of o)) . ((Den (o,(Free (S,Z)))) . m)
by A9, MSAFREE4:def 10, MSUALG_3:def 7
.=
((canonical_homomorphism R) . (the_result_sort_of o)) . (o -term m)
by MSAFREE4:13
.=
((canonical_homomorphism R) . (the_sort_of (o -term m))) . (o -term m)
by Th8
.=
(canonical_homomorphism R) . (o -term m)
by ABBR
.=
(canonical_homomorphism R) . (C -sub (@ ((canonical_homomorphism R) . t)))
by C1, A4, A6, Th43
;
hence
S1[
C]
;
verum end;
thus
S1[C9]
from MSAFREE5:sch 4(A2, A3); verum