reconsider o = ~ the rmult of W as Function of [: the carrier of (opp K), the carrier of W:], the carrier of W ;

take ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ; :: thesis: for o being Function of [: the carrier of (opp K), the carrier of W:], the carrier of W st o = ~ the rmult of W holds

ModuleStr(# the carrier of W, the addF of W,(0. W),o #) = ModuleStr(# the carrier of W, the addF of W,(0. W),o #)

thus for o being Function of [: the carrier of (opp K), the carrier of W:], the carrier of W st o = ~ the rmult of W holds

ModuleStr(# the carrier of W, the addF of W,(0. W),o #) = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ; :: thesis: verum

take ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ; :: thesis: for o being Function of [: the carrier of (opp K), the carrier of W:], the carrier of W st o = ~ the rmult of W holds

ModuleStr(# the carrier of W, the addF of W,(0. W),o #) = ModuleStr(# the carrier of W, the addF of W,(0. W),o #)

thus for o being Function of [: the carrier of (opp K), the carrier of W:], the carrier of W st o = ~ the rmult of W holds

ModuleStr(# the carrier of W, the addF of W,(0. W),o #) = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ; :: thesis: verum