reconsider o = ~ the rmult of W as Function of [:the carrier of (opp K),the carrier of W:],the carrier of W ;
take VectSpStr(# 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
VectSpStr(# the carrier of W,the addF of W,(0. W),o #) = VectSpStr(# 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
VectSpStr(# the carrier of W,the addF of W,(0. W),o #) = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) ; :: thesis: verum