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

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

assume A2: p in dom powerSCMFunction ; :: thesis: ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)
then powerSCMFunction . p in FinPartSt SCM by PARTFUN1:4;
then A3: powerSCMFunction . 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,1) & powerSCMFunction . p = (dl. 2) .--> H₂(n) ) by A1, A2, A3, Def5;
hence ex n being Nat st p = ((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1) ; :: thesis: verum

end;

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