let F1, F2 be Function of V,(); :: thesis: ( F1 is one-to-one & ( for v being Element of V holds F1 . v = Class ((),[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. () & F2 is one-to-one & ( for v being Element of V holds F2 . v = Class ((),[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. () implies F1 = F2 )

assume A1: ( F1 is one-to-one & ( for v being Element of V holds F1 . v = Class ((),[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. () ) ; :: thesis: ( not F2 is one-to-one or ex v being Element of V st not F2 . v = Class ((),[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. () or F1 = F2 )

assume A2: ( F2 is one-to-one & ( for v being Element of V holds F2 . v = Class ((),[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. () ) ; :: thesis: F1 = F2
now :: thesis: for v being Element of V holds F1 . v = F2 . v
let v be Element of V; :: thesis: F1 . v = F2 . v
thus F1 . v = Class ((),[v,1]) by A1
.= F2 . v by A2 ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:def 8; :: thesis: verum