reconsider A = a as Element of SCM-Data-Loc by Th1;
s . A in the carrier of R ;
hence s . a is Element of R ; :: thesis: verum