let F1, F2 be Function of (TOP-REAL n),(TOP-REAL m); :: thesis: ( ( n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 ) )
A8: now :: thesis: ( n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 )
assume n <> 0 ; :: thesis: ( ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 )
assume A9: for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ; :: thesis: ( ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 )
assume A10: for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ; :: thesis: F1 = F2
now :: thesis: for x being Element of (TOP-REAL n) holds F1 . x = F2 . x
let x be Element of (TOP-REAL n); :: thesis: F1 . x = F2 . x
thus F1 . x = Line (((LineVec2Mx (@ x)) * M),1) by A9
.= F2 . x by A10 ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; :: thesis: verum
end;
now :: thesis: ( n = 0 & ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 )
assume n = 0 ; :: thesis: ( ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 )
assume A11: for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ; :: thesis: ( ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 )
assume A12: for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ; :: thesis: F1 = F2
now :: thesis: for x being Element of (TOP-REAL n) holds F1 . x = F2 . x
let x be Element of (TOP-REAL n); :: thesis: F1 . x = F2 . x
thus F1 . x = 0. (TOP-REAL m) by A11
.= F2 . x by A12 ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; :: thesis: verum
end;
hence ( ( n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 ) ) by A8; :: thesis: verum