consider o, m being set ;
take CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) ; :: thesis: ( not CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is void & not CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is empty )
thus ( not CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is void & not CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is empty ) ; :: thesis: verum