let S be non empty non void ManySortedSign ; :: thesis: 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 C9 being context of z st C9 is basic holds
transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9
let s be SortSymbol of S; :: thesis: for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z st C9 is basic holds
transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis: for z being Element of Z . s
for C9 being context of z st C9 is basic holds
transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9
let z be Element of Z . s; :: thesis: for C9 being context of z st C9 is basic holds
transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9
let C9 be context of z; :: thesis: ( C9 is basic implies transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9 )
set X = Z;
set C = C9;
set x = z;
given o being OperSymbol of S, k being Element of Args (o,(Free (S,Z))) such that Z0: ( C9 = o -term k & z -context_in k = z -term ) ; :: according to MSAFREE5:def 34 :: thesis: transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9
set p = k;
take o ; :: according to MSUALG_6:def 5 :: thesis: ( the_result_sort_of o = the_sort_of C9 & ex b₁ being Element of omega st
( b₁ in dom (the_arity_of o) & (the_arity_of o) /. b₁ = s & ex b₂ being set st
( b₂ in Args (o,(Free (S,Z))) & transl C9 = transl (o,b₁,b₂,(Free (S,Z))) ) ) )
thus the_result_sort_of o = the_sort_of C9 by Z0, Th8; :: thesis: ex b₁ being Element of omega st
( b₁ in dom (the_arity_of o) & (the_arity_of o) /. b₁ = s & ex b₂ being set st
( b₂ in Args (o,(Free (S,Z))) & transl C9 = transl (o,b₁,b₂,(Free (S,Z))) ) )
reconsider i = z -context_pos_in k as Element of NAT by ORDINAL1:def 12;
take i ; :: thesis: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s & ex b₁ being set st
( b₁ in Args (o,(Free (S,Z))) & transl C9 = transl (o,i,b₁,(Free (S,Z))) ) )
A1: k is z -context_including by Z0, Th53;
then i in dom k by Th71;
hence i in dom (the_arity_of o) by MSUALG_3:6; :: thesis: ( (the_arity_of o) /. i = s & ex b₁ being set st
( b₁ in Args (o,(Free (S,Z))) & transl C9 = transl (o,i,b₁,(Free (S,Z))) ) )
then ( z -term = k . i & k . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) ) by Z0, A1, Th71, MSUALG_6:2;
then A4: ( s = the_sort_of (z -context_in k) & the_sort_of (z -context_in k) = (the_arity_of o) /. i ) by Z0, SORT;
hence (the_arity_of o) /. i = s ; :: thesis: ex b₁ being set st
( b₁ in Args (o,(Free (S,Z))) & transl C9 = transl (o,i,b₁,(Free (S,Z))) )
reconsider a = k as Function ;
take a ; :: thesis: ( a in Args (o,(Free (S,Z))) & transl C9 = transl (o,i,a,(Free (S,Z))) )
thus a in Args (o,(Free (S,Z))) ; :: thesis: transl C9 = transl (o,i,a,(Free (S,Z)))
dom (transl C9) = the Sorts of (Free (S,Z)) . s by FUNCT_2:def 1;
hence dom (transl C9) = dom (transl (o,i,a,(Free (S,Z)))) by A4, MSUALG_6:def 4; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 (transl C9) or (transl C9) . b₁ = (transl (o,i,a,(Free (S,Z)))) . b₁ )
let c be object ; :: thesis: ( not c in proj1 (transl C9) or (transl C9) . c = (transl (o,i,a,(Free (S,Z)))) . c )
assume c in dom (transl C9) ; :: thesis: (transl C9) . c = (transl (o,i,a,(Free (S,Z)))) . c
then reconsider c = c as Element of the Sorts of (Free (S,Z)) . s ;
reconsider q = k +* (i,c) as Element of Args (o,(Free (S,Z))) by A4, MSUALG_6:7;
A6: (transl (o,i,a,(Free (S,Z)))) . c = (Den (o,(Free (S,Z)))) . q by A4, MSUALG_6:def 4
.= o -term q by MSAFREE4:13 ;
( C9 -sub c = o -term q & the_sort_of c = s ) by Z0, Th58, SORT;
hence (transl C9) . c = (transl (o,i,a,(Free (S,Z)))) . c by A6, TRANS; :: thesis: verum