let V be free Z_Module; :: thesis: for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( IQ = (MorphsZQ V) .: I implies card I = card IQ )

assume AS1: IQ = (MorphsZQ V) .: I ; :: thesis: card I = card IQ

P1: MorphsZQ V is one-to-one by defMorph;

the carrier of V = dom (MorphsZQ V) by FUNCT_2:def 1;

hence card I = card IQ by AS1, P1, CARD_1:5, CARD_1:33; :: thesis: verum

for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds

card I = card IQ

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( IQ = (MorphsZQ V) .: I implies card I = card IQ )

assume AS1: IQ = (MorphsZQ V) .: I ; :: thesis: card I = card IQ

P1: MorphsZQ V is one-to-one by defMorph;

the carrier of V = dom (MorphsZQ V) by FUNCT_2:def 1;

hence card I = card IQ by AS1, P1, CARD_1:5, CARD_1:33; :: thesis: verum