let g1, g2 be FinPartState of SCM+FSA ; :: thesis: ( dom g1 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom g1 holds
g1 . k = f /. (k + 1) ) & dom g2 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom g2 holds
g2 . k = f /. (k + 1) ) implies g1 = g2 )
assume that
A14: ( dom g1 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom g1 holds
g1 . k = f /. (k + 1) ) ) and
A15: ( dom g2 = { (m -' 1) where m is Element of NAT : m in dom f } & ( for k being Element of NAT st k in dom g2 holds
g2 . k = f /. (k + 1) ) ) ; :: thesis: g1 = g2

now

let x be set ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A16: x in dom g1 ; :: thesis: g1 . x = g2 . x
then consider k1 being Element of NAT such that
A17: x = k1 -' 1 and
k1 in dom f by A14;
reconsider k = k1 -' 1 as Element of NAT ;
g2 . k = f /. (k + 1) by A14, A15, A16, A17;
hence g1 . x = g2 . x by A14, A16, A17; :: thesis: verum

end;

hence g1 = g2 by A14, A15, FUNCT_1:9; :: thesis: verum