:: The Inner Product of Finite Sequences and of Points of $n$-dimensionalTopological Space
:: by Kanchun and Yatsuka Nakamura
::
:: Received February 3, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: EUCLID_2:1
theorem Th2: :: EUCLID_2:2
theorem :: EUCLID_2:3
theorem :: EUCLID_2:4
theorem Th5: :: EUCLID_2:5
theorem Th6: :: EUCLID_2:6
theorem Th7: :: EUCLID_2:7
theorem Th8: :: EUCLID_2:8
theorem Th9: :: EUCLID_2:9
:: deftheorem defines |( EUCLID_2:def 1 :
theorem Th10: :: EUCLID_2:10
theorem Th11: :: EUCLID_2:11
theorem Th12: :: EUCLID_2:12
theorem Th13: :: EUCLID_2:13
theorem Th14: :: EUCLID_2:14
theorem Th15: :: EUCLID_2:15
theorem :: EUCLID_2:16
theorem Th17: :: EUCLID_2:17
theorem :: EUCLID_2:18
theorem Th19: :: EUCLID_2:19
theorem Th20: :: EUCLID_2:20
theorem Th21: :: EUCLID_2:21
theorem Th22: :: EUCLID_2:22
theorem :: EUCLID_2:23
theorem :: EUCLID_2:24
theorem Th25: :: EUCLID_2:25
theorem :: EUCLID_2:26
theorem :: EUCLID_2:27
theorem :: EUCLID_2:28
theorem Th29: :: EUCLID_2:29
theorem Th30: :: EUCLID_2:30
theorem Th31: :: EUCLID_2:31
theorem Th32: :: EUCLID_2:32
theorem Th33: :: EUCLID_2:33
theorem Th34: :: EUCLID_2:34
theorem :: EUCLID_2:35
theorem :: EUCLID_2:36
theorem Th37: :: EUCLID_2:37
theorem :: EUCLID_2:38
definition
canceled;
end;
:: deftheorem EUCLID_2:def 2 :
canceled;
theorem :: EUCLID_2:39
theorem Th40: :: EUCLID_2:40
theorem Th41: :: EUCLID_2:41
theorem :: EUCLID_2:42
theorem Th43: :: EUCLID_2:43
theorem :: EUCLID_2:44
theorem :: EUCLID_2:45
theorem Th46: :: EUCLID_2:46
theorem :: EUCLID_2:47
theorem :: EUCLID_2:48
theorem :: EUCLID_2:49
theorem Th50: :: EUCLID_2:50
theorem Th51: :: EUCLID_2:51
theorem Th52: :: EUCLID_2:52
theorem Th53: :: EUCLID_2:53
theorem Th54: :: EUCLID_2:54
theorem :: EUCLID_2:55
theorem :: EUCLID_2:56
theorem Th57: :: EUCLID_2:57
theorem Th58: :: EUCLID_2:58
theorem Th59: :: EUCLID_2:59
theorem Th60: :: EUCLID_2:60
theorem Th61: :: EUCLID_2:61
theorem Th62: :: EUCLID_2:62
theorem Th63: :: EUCLID_2:63
theorem :: EUCLID_2:64
theorem :: EUCLID_2:65
theorem :: EUCLID_2:66
theorem Th67: :: EUCLID_2:67
theorem Th68: :: EUCLID_2:68
theorem :: EUCLID_2:69
theorem :: EUCLID_2:70
theorem :: EUCLID_2:71
theorem :: EUCLID_2:72
theorem Th73: :: EUCLID_2:73
theorem :: EUCLID_2:74
:: deftheorem Def3 defines are_orthogonal EUCLID_2:def 3 :
theorem Th75: :: EUCLID_2:75
theorem :: EUCLID_2:76
theorem Th77: :: EUCLID_2:77
theorem Th78: :: EUCLID_2:78
theorem :: EUCLID_2:79
theorem :: EUCLID_2:80