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