take AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) ; :: thesis: ( AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is strict & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is Abelian & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is add-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_zeroed & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_complementable & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is commutative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_unital & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is mix-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is vector-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-distributive )
thus ( AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is strict & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is Abelian & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is add-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_zeroed & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_complementable & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is commutative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_unital & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is mix-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is vector-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-distributive ) ; :: thesis: verum