reconsider o = ~ the rmult of W as Function of [:the carrier of (opp K),the carrier of W:],the carrier of W ;
let M1, M2 be strict VectSpStr of opp K; :: 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
M1 = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) ) & ( 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
M2 = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) ) implies M1 = M2 )
assume that
A1: 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
M1 = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) and
A2: 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
M2 = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) ; :: thesis: M1 = M2
thus M1 = VectSpStr(# the carrier of W,the addF of W,(0. W),o #) by A1
.= M2 by A2 ; :: thesis: verum