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