let F1, F2 be Function of V,(Z_MQ_VectSp V); :: thesis: ( F1 is one-to-one & ( for v being Element of V holds F1 . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F1 . (v + w) = (F1 . v) + (F1 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F1 . (i * v) = q * (F1 . v) ) & F1 . (0. V) = 0. (Z_MQ_VectSp V) & F2 is one-to-one & ( for v being Element of V holds F2 . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F2 . (v + w) = (F2 . v) + (F2 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F2 . (i * v) = q * (F2 . v) ) & F2 . (0. V) = 0. (Z_MQ_VectSp V) implies F1 = F2 )
assume A1: ( F1 is one-to-one & ( for v being Element of V holds F1 . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F1 . (v + w) = (F1 . v) + (F1 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F1 . (i * v) = q * (F1 . v) ) & F1 . (0. V) = 0. (Z_MQ_VectSp V) ) ; :: thesis: ( not F2 is one-to-one or ex v being Element of V st not F2 . v = Class ((EQRZM V),[v,1]) or ex v, w being Element of V st not F2 . (v + w) = (F2 . v) + (F2 . w) or ex v being Element of V ex i being Element of INT.Ring ex q being Element of F_Rat st
( i = q & not F2 . (i * v) = q * (F2 . v) ) or not F2 . (0. V) = 0. (Z_MQ_VectSp V) or F1 = F2 )
assume A2: ( F2 is one-to-one & ( for v being Element of V holds F2 . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds F2 . (v + w) = (F2 . v) + (F2 . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F2 . (i * v) = q * (F2 . v) ) & F2 . (0. V) = 0. (Z_MQ_VectSp V) ) ; :: thesis: F1 = F2
hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum