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