let F1, F2 be RFunctional of V; :: thesis: ( ( for v being Element of V holds F1 . v = l . (i_FC * v) ) & ( for v being Element of V holds F2 . v = l . (i_FC * v) ) implies F1 = F2 )
assume that
A2: for v being Element of V holds F1 . v = l . (i_FC * v) and
A3: for v being Element of V holds F2 . v = l . (i_FC * v) ; :: 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 = l . (i_FC * v) by A2
.= F2 . v by A3 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum