let UN be Universe; :: thesis: ( the carrier of Z3 in UN & the addF of Z3 in UN & comp Z3 in UN & 0. Z3 in UN & the multF of Z3 in UN & 1. Z3 in UN )
thus the carrier of Z3 in UN by Lm8; :: thesis: ( the addF of Z3 in UN & comp Z3 in UN & 0. Z3 in UN & the multF of Z3 in UN & 1. Z3 in UN )
hence ( the addF of Z3 in UN & comp Z3 in UN & 0. Z3 in UN & the multF of Z3 in UN & 1. Z3 in UN ) by Lm9, GRCAT_1:4; :: thesis: verum