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
transl C2 = (transl C1) * (transl C)
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
transl C2 = (transl C1) * (transl C)
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
transl C2 = (transl C1) * (transl C)
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
transl C2 = (transl C1) * (transl C)
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
transl C2 = (transl C1) * (transl C) )
assume that
ZZ: X is non-trivial and
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
transl C2 = (transl C1) * (transl C)
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
transl C2 = (transl C1) * (transl C)
let C1 be context of x1; :: thesis: for C2 being context of x st C2 = C1 -sub C holds
transl C2 = (transl C1) * (transl C)
let C2 be context of x; :: thesis: ( C2 = C1 -sub C implies transl C2 = (transl C1) * (transl C) )
assume Z1: C2 = C1 -sub C ; :: thesis: transl C2 = (transl C1) * (transl C)
reconsider f = transl C as Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . s1) by Z0;
transl C2 = (transl C1) * f
proof
let t be Element of the Sorts of (Free (S,X)) . s; :: according to PBOOLE:def 21 :: thesis: (transl C2) . t = ((transl C1) * f) . t
A1: the_sort_of t = s by SORT;
then A2: ( (transl C2) . t = C2 -sub t & (transl C) . t = C -sub t ) by TRANS;
the_sort_of (C -sub t) = s1 by Z0, SORT;
then (transl C1) . (C -sub t) = C1 -sub (C -sub t) by TRANS;
then ((transl C1) * f) . t = C1 -sub (C -sub t) by A2, FUNCT_2:15;
hence (transl C2) . t = ((transl C1) * f) . t by ZZ, A2, Z0, Z1, A1, Th60; :: thesis: verum
end;
hence transl C2 = (transl C1) * (transl C) ; :: thesis: verum