let p be prime Element of INT.Ring; :: thesis: for V being Z_Module
for v, w being Vector of V st (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} holds
ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)
let V be Z_Module; :: thesis: for v, w being Vector of V st (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} holds
ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)
let v, w be Vector of V; :: thesis: ( (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} implies ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v) )
assume A1: (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} ; :: thesis: ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)
consider u being object such that
A2: u in (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) by A1, XBOOLE_0:def 1;
A3: ( u in ZMtoMQV (V,p,w) & u in ZMtoMQV (V,p,v) ) by A2, XBOOLE_0:def 4;
then reconsider u = u as Vector of V ;
w + (p (*) V) = u + (p (*) V) by A3, ZMODUL01:67
.= v + (p (*) V) by A3, ZMODUL01:67 ;
hence ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v) ; :: thesis: verum