defpred S₁[ set , set ] means ex k being Element of NAT st
( $1 = k -' 1 & $2 = f /. k & k in dom f );
set X = { H₁(m) where m is Element of NAT : m in dom f } ;
A1: for e being set st e in { H₁(m) where m is Element of NAT : m in dom f } holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in { H₁(m) where m is Element of NAT : m in dom f } implies ex u being set st S₁[e,u] )
assume e in { H₁(m) where m is Element of NAT : m in dom f } ; :: thesis: ex u being set st S₁[e,u]
then consider k being Element of NAT such that
A2: ( e = k -' 1 & k in dom f ) ;
take f /. k ; :: thesis: S₁[e,f /. k]
take k ; :: thesis: ( e = k -' 1 & f /. k = f /. k & k in dom f )
thus ( e = k -' 1 & f /. k = f /. k & k in dom f ) by A2; :: thesis: verum

end;

consider g being Function such that
A3: ( dom g = { H₁(m) where m is Element of NAT : m in dom f } & ( for e being set st e in { H₁(m) where m is Element of NAT : m in dom f } holds
S₁[e,g . e] ) ) from CLASSES1:sch 1(A1);
A5: dom g c= the carrier of SCM+FSA

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in the carrier of SCM+FSA )
assume x in dom g ; :: thesis: x in the carrier of SCM+FSA
then ex k being Element of NAT st
( x = k -' 1 & k in dom f ) by A3;
then x is Element of NAT ;
then X: x in NAT ;
thus x in the carrier of SCM+FSA by X; :: thesis: verum

end;

A6: now

let x be set ; :: thesis: ( x in dom g implies g . x in the Object-Kind of SCM+FSA . x )
assume x in dom g ; :: thesis: g . x in the Object-Kind of SCM+FSA . x
then consider k being Element of NAT such that
A7: x = k -' 1 and
A8: g . x = f /. k and
k in dom f by A3;
the Object-Kind of SCM+FSA . x = the Object-Kind of SCM+FSA . (k -' 1) by A7
.= the Instructions of SCM+FSA by COMPOS_1:def 8 ;
hence g . x in the Object-Kind of SCM+FSA . x by A8; :: thesis: verum

end;

A9: dom f is finite ;
{ H₁(m) where m is Element of NAT : m in dom f } is finite from FRAENKEL:sch 21(A9);
then reconsider g = g as FinPartState of SCM+FSA by A3, A5, A6, FINSET_1:29, FUNCT_1:def 20, RELAT_1:def 18;
take g ; :: thesis: ( dom g = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom g holds
g . k = f /. (k + 1) ) )
thus dom g = { (m -' 1) where m is Element of NAT : m in dom f } by A3; :: thesis: for k being Element of NAT st k in dom g holds
g . k = f /. (k + 1)
let k be Element of NAT ; :: thesis: ( k in dom g implies g . k = f /. (k + 1) )
assume k in dom g ; :: thesis: g . k = f /. (k + 1)
then consider a being Element of NAT such that
A10: k = a -' 1 and
A11: g . k = f /. a and
A12: a in dom f by A3;
A13: ( k + 1 >= 1 & (k + 1) -' 1 = a -' 1 ) by A10, NAT_1:11, NAT_D:34;
ex n being Nat st dom f = Seg n by FINSEQ_1:def 2;
then a >= 1 by A12, FINSEQ_1:3;
hence g . k = f /. (k + 1) by A11, A13, XREAL_1:236; :: thesis: verum