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

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