let p be object ; :: thesis: ( p in dom sumSCMFunction iff ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) )
A1: ( p in dom sumSCMFunction iff [p,(sumSCMFunction . p)] in sumSCMFunction ) by FUNCT_1:1;

hereby :: thesis: ( ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) implies p in dom sumSCMFunction )

assume A2: p in dom sumSCMFunction ; :: thesis: ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0)
then sumSCMFunction . p in FinPartSt SCM by PARTFUN1:4;
then A3: sumSCMFunction . p is FinPartState of SCM by MEMSTR_0:76;
p is FinPartState of SCM by A2, MEMSTR_0:76;
then ex n being Nat st
( p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) & sumSCMFunction . p = (dl. 2) .--> H₁(n) ) by A1, A2, A3, Def6;
hence ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) ; :: thesis: verum

end;

given n being Nat such that A4: p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0) ; :: thesis: p in dom sumSCMFunction
[p,((dl. 2) .--> H₁(n))] in sumSCMFunction by A4, Def6;
hence p in dom sumSCMFunction by FUNCT_1:1; :: thesis: verum