let IT1, IT2 be preProgram of SCM+FSA ; :: thesis: ( dom IT1 = dom p & ( for m being Element of NAT st m in dom p holds
IT1 . m = IncAddr (pi p,m),k ) & dom IT2 = dom p & ( for m being Element of NAT st m in dom p holds
IT2 . m = IncAddr (pi p,m),k ) implies IT1 = IT2 )
assume that
A9: dom IT1 = dom p and
A10: for m being Element of NAT st m in dom p holds
IT1 . m = IncAddr (pi p,m),k and
A11: dom IT2 = dom p and
A12: for m being Element of NAT st m in dom p holds
IT2 . 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 A13: x in dom p ; :: thesis: IT1 . x = IT2 . x
dom p c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A13;
reconsider m = l as Element of NAT ;
thus IT1 . x = IncAddr (pi p,m),k by A10, A13
.= IT2 . x by A12, A13 ; :: thesis: verum

end;

hence IT1 = IT2 by A9, A11, FUNCT_1:9; :: thesis: verum