let a, b be Int-Location; :: thesis: MultBy (a,b) = [4,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & MultBy (a,b) = MultBy (A,B) ) by SCMFSA_2:def 11;
hence MultBy (a,b) = [4,{},<*a,b*>] ; :: thesis: verum