let n be Nat; :: thesis: powerSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)) = (dl. 2) .--> (n !)
[(((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)),((dl. 2) .--> H₂(n))] in powerSCMFunction by Def5;
hence powerSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)) = (dl. 2) .--> (n !) by FUNCT_1:1; :: thesis: verum