let IT1, IT2 be preProgram of SCM+FSA ; :: thesis: ( dom IT1 = dom p & ( for m being Element of NAT st insloc m in dom p holds
IT1 . (insloc m) = IncAddr (pi p,m),k ) & dom IT2 = dom p & ( for m being Element of NAT st insloc m in dom p holds
IT2 . (insloc m) = IncAddr (pi p,m),k ) implies IT1 = IT2 )
assume that
A12: dom IT1 = dom p and
A13: for m being Element of NAT st insloc m in dom p holds
IT1 . (insloc m) = IncAddr (pi p,m),k and
A14: dom IT2 = dom p and
A15: for m being Element of NAT st insloc m in dom p holds
IT2 . (insloc m) = IncAddr (pi p,m),k ; :: thesis: IT1 = IT2
for x being set st x in dom p holds
IT1 . x = IT2 . x

proof

let x be set ; :: thesis: ( x in dom p implies IT1 . x = IT2 . x )
assume A16: x in dom p ; :: thesis: IT1 . x = IT2 . x
dom p c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A16, AMI_1:def 4;
reconsider m = l as Element of NAT by ORDINAL1:def 13;
A17: l = insloc m ;
hence IT1 . x = IncAddr (pi p,m),k by A13, A16
.= IT2 . x by A15, A16, A17 ;
:: thesis: verum

end;

hence IT1 = IT2 by A12, A14, FUNCT_1:9; :: thesis: verum