let n be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA
for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) holds
for s being preProgram of SCM+FSA holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
let i be Instruction of SCM+FSA ; :: thesis: for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) holds
for s being preProgram of SCM+FSA holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
let f be Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA ; :: thesis: ( f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) implies for s being preProgram of SCM+FSA holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n) )
assume A1: f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) ; :: thesis: for s being preProgram of SCM+FSA holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
A2: dom ((halt SCM+FSA ) .--> (IncAddr i,n)) = {(halt SCM+FSA )} by FUNCOP_1:19;
A3: dom ((halt SCM+FSA ) .--> i) = {(halt SCM+FSA )} by FUNCOP_1:19;
A4: rng ((halt SCM+FSA ) .--> (IncAddr i,n)) = {(IncAddr i,n)} by FUNCOP_1:14;
A5: dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
A6: dom ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) = (dom (id the Instructions of SCM+FSA )) \/ {(halt SCM+FSA )} by A2, FUNCT_4:def 1
.= the Instructions of SCM+FSA by A5, ZFMISC_1:46 ;
A7: rng (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
A8: rng ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) c= (rng (id the Instructions of SCM+FSA )) \/ {(IncAddr i,n)} by A4, FUNCT_4:18;
(rng (id the Instructions of SCM+FSA )) \/ {(IncAddr i,n)} = the Instructions of SCM+FSA by A7, ZFMISC_1:46;
then reconsider g = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n)) as Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA by A6, A8, FUNCT_2:def 1, RELSET_1:11;
let s be preProgram of SCM+FSA ; :: thesis: IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
A9: dom (g * (IncAddr s,n)) = dom (IncAddr s,n) by AMI_1:119;
A10: dom (IncAddr s,n) = dom s by Def6
.= dom (f * s) by AMI_1:119 ;

now

let m be Element of NAT ; :: thesis: ( insloc m in dom (f * s) implies (g * (IncAddr s,n)) . (insloc b₁) = IncAddr (pi (f * s),b₁),n )
assume A11: insloc m in dom (f * s) ; :: thesis: (g * (IncAddr s,n)) . (insloc b₁) = IncAddr (pi (f * s),b₁),n
then A12: insloc m in dom s by AMI_1:119;

per cases ( s . (insloc m) = halt SCM+FSA or s . (insloc m) <> halt SCM+FSA ) ;

suppose A13: s . (insloc m) = halt SCM+FSA ; :: thesis: (g * (IncAddr s,n)) . (insloc b₁) = IncAddr (pi (f * s),b₁),n

A14: (IncAddr s,n) . (insloc m) = IncAddr (pi s,m),n by A12, Th24
.= IncAddr (halt SCM+FSA ),n by A12, A13, AMI_1:def 47
.= halt SCM+FSA by Th8 ;
A15: halt SCM+FSA in {(halt SCM+FSA )} by TARSKI:def 1;
A16: pi (f * s),m = (f * s) . (insloc m) by A11, AMI_1:def 47
.= f . (halt SCM+FSA ) by A12, A13, FUNCT_1:23
.= ((halt SCM+FSA ) .--> i) . (halt SCM+FSA ) by A1, A3, A15, FUNCT_4:14
.= i by FUNCOP_1:87 ;
thus (g * (IncAddr s,n)) . (insloc m) = g . ((IncAddr s,n) . (insloc m)) by A10, A11, FUNCT_1:23
.= ((halt SCM+FSA ) .--> (IncAddr i,n)) . ((IncAddr s,n) . (insloc m)) by A2, A14, A15, FUNCT_4:14
.= IncAddr (pi (f * s),m),n by A14, A16, FUNCOP_1:87 ; :: thesis: verum

end;

suppose A17: s . (insloc m) <> halt SCM+FSA ; :: thesis: (g * (IncAddr s,n)) . (insloc b₁) = IncAddr (pi (f * s),b₁),n

A18: pi s,m = s . (insloc m) by A12, AMI_1:def 47;
then A19: InsCode (pi s,m) <> 0 by A17, SCMFSA_2:122;
InsCode (IncAddr (pi s,m),n) = InsCode (pi s,m) by Th22;
then A20: not IncAddr (pi s,m),n in {(halt SCM+FSA )} by A19, SCMFSA_2:124, TARSKI:def 1;
A21: not pi s,m in {(halt SCM+FSA )} by A17, A18, TARSKI:def 1;
A22: pi (f * s),m = (f * s) . (insloc m) by A11, AMI_1:def 47
.= f . (s . (insloc m)) by A12, FUNCT_1:23
.= (id the Instructions of SCM+FSA ) . (pi s,m) by A1, A3, A18, A21, FUNCT_4:12
.= pi s,m by FUNCT_1:35 ;
thus (g * (IncAddr s,n)) . (insloc m) = g . ((IncAddr s,n) . (insloc m)) by A10, A11, FUNCT_1:23
.= g . (IncAddr (pi s,m),n) by A12, Def6
.= (id the Instructions of SCM+FSA ) . (IncAddr (pi s,m),n) by A2, A20, FUNCT_4:12
.= IncAddr (pi (f * s),m),n by A22, FUNCT_1:35 ; :: thesis: verum

end;

end;

end;

hence IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n) by A9, A10, Def6; :: thesis: verum