reconsider A = a, B = b as Data-Location by Th5;
reconsider i = MultBy (A,B) as Instruction of SCM+FSA by Th10;
take i ; :: thesis: ex A, B being Data-Location st
( a = A & b = B & i = MultBy (A,B) )
take A ; :: thesis: ex B being Data-Location st
( a = A & b = B & i = MultBy (A,B) )
take B ; :: thesis: ( a = A & b = B & i = MultBy (A,B) )
thus ( a = A & b = B & i = MultBy (A,B) ) ; :: thesis: verum