deffunc H₁( set , Element of the carrier of S * ) -> Element of K21(K22(((len c₂) -tuples_on BOOLEAN ),BOOLEAN )) = ((len c₂) -tuples_on BOOLEAN ) --> FALSE ;
A1: for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN ),BOOLEAN ;
consider A being strict MSAlgebra of S such that
A2: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H₁(g,p) ) ) from CIRCCOMB:sch 2(A1);
take A ; :: thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def 15 :: thesis: the Sorts of A . v = BOOLEAN
thus the Sorts of A . v = BOOLEAN by A2, FUNCOP_1:13; :: thesis: verum