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 C being context of x st C = x -term holds
transl C = id ( the Sorts of (Free (S,X)) . s)
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 C being context of x st C = x -term holds
transl C = id ( the Sorts of (Free (S,X)) . s)
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 C = x -term holds
transl C = id ( the Sorts of (Free (S,X)) . s)
let x be Element of X . s; :: thesis: for C being context of x st C = x -term holds
transl C = id ( the Sorts of (Free (S,X)) . s)
let C be context of x; :: thesis: ( C = x -term implies transl C = id ( the Sorts of (Free (S,X)) . s) )
assume Z0: C = x -term ; :: thesis: transl C = id ( the Sorts of (Free (S,X)) . s)
let t be Element of the Sorts of (Free (S,X)) . s; :: according to PBOOLE:def 21 :: thesis: (transl C) . t = (id ( the Sorts of (Free (S,X)) . s)) . t
A2: the_sort_of t = s by SORT;
hence (transl C) . t = C -sub t by TRANS
.= (id ( the Sorts of (Free (S,X)) . s)) . t by Z0, A2, Th41 ;
:: thesis: verum