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

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

now :: thesis: for v being Element of V holds F1 . v = F2 . v

hence
F1 = F2
by FUNCT_2:def 8; :: thesis: verumlet v be Element of V; :: thesis: F1 . v = F2 . v

thus F1 . v = Class ((EQRZM V),[v,1]) by A1

.= F2 . v by A2 ; :: thesis: verum

end;thus F1 . v = Class ((EQRZM V),[v,1]) by A1

.= F2 . v by A2 ; :: thesis: verum