let n be Nat; :: thesis: sumSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0)) = (dl. 2) .--> (Triangle n)
[(((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0)),((dl. 2) .--> H₁(n))] in sumSCMFunction by Def6;
hence sumSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,0)) = (dl. 2) .--> (Triangle n) by FUNCT_1:1; :: thesis: verum