let a, b be Functional of V; :: thesis: ( ( for v being Element of V holds a . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) & ( for v being Element of V holds b . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ) implies a = b )
assume A2: for v being Element of V holds a . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ; :: thesis: ( ex v being Element of V st not b . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] or a = b )
assume A3: for v being Element of V holds b . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] ; :: thesis: a = b

now :: thesis: for v being Element of V holds a . v = b . v

let v be Element of V; :: thesis: a . v = b . v
thus a . v = [**((RtoC l) . v),(- ((i-shift (RtoC l)) . v))**] by A2
.= b . v by A3 ; :: thesis: verum

end;

hence a = b by FUNCT_2:63; :: thesis: verum