let m be Element of NAT ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let o be OperSymbol of S; :: thesis:
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis:
let q be Element of Args (o,(Free (S,Y))); :: thesis:
let s1, s2 be SortSymbol of S; :: thesis:
let V be finite set ; :: thesis:
assume Z1: m in dom q ; :: thesis:
assume Z2: s1 = (the_arity_of o) /. m ; :: thesis:
consider y being Element of Y . s1, C being context of y, q1 being Element of Args (o,(Free (S,Y))) such that
A1: ( y nin V & C = o -term q1 & q1 = q +* (m,(y -term)) & q1 is y -context_including & m = y -context_pos_in q1 & y -context_in q1 = y -term ) by Z1, Z2, Th59;
take y ; :: thesis:
take C ; :: thesis:
take q1 ; :: thesis:
thus y nin V by A1; :: thesis:
thus q1 = q +* (m,(y -term)) by A1; :: thesis:
thus q1 is y -context_including by A1; :: thesis:
thus y -context_in q1 = y -term by A1; :: thesis:
thus C = o -term q1 by A1; :: thesis:
thus m = y -context_pos_in q1 by A1; :: thesis:
dom (transl C) = the Sorts of (Free (S,Y)) . s1 by FUNCT_2:def 1;
hence dom (transl C) = dom (transl (o,m,q,(Free (S,Y)))) by Z2, MSUALG_6:def 4; :: according to FUNCT_1:def 11 :: thesis:
let c be object ; :: thesis:
assume c in dom (transl C) ; :: thesis:
then reconsider c = c as Element of the Sorts of (Free (S,Y)) . s1 ;
reconsider q2 = q +* (m,c) as Element of Args (o,(Free (S,Y))) by Z2, MSUALG_6:7;
A6: (transl (o,m,q,(Free (S,Y)))) . c = (Den (o,(Free (S,Y)))) . q2 by Z2, MSUALG_6:def 4
.= o -term q2 by MSAFREE4:13 ;
q2 = q1 +* (m,c) by A1, FUNCT_7:34;
then ( C -sub c = o -term q2 & the_sort_of c = s1 ) by A1, Th58, SORT;
hence (transl C) . c = (transl (o,m,q,(Free (S,Y)))) . c by A6, TRANS; :: thesis: