:: BHSP_1 semantic presentation

definition

attr a₁ is strict;
struct UNITSTR -> RLSStruct ;
aggr UNITSTR(# carrier, Zero, add, Mult, scalar #) -> UNITSTR ;
sel scalar c₁ -> Function of [:the carrier of a₁,the carrier of a₁:], REAL ;

end;

registration

cluster non empty strict UNITSTR ;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:REAL ,c₁:],c₁;
let c₅ be Function of [:c₁,c₁:], REAL ;
cluster UNITSTR(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence

proof end;

end;

deffunc H₁( UNITSTR ) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be non empty UNITSTR ;
let c₂, c₃ be Point of c₁;
func c₂ .|. c₃ -> Real equals :: BHSP_1:def 1
the scalar of a₁ . [a₂,a₃];
correctness ;

end;

:: deftheorem Def1 defines .|. BHSP_1:def 1 :

consider c₁ being RealLinearSpace;

Lemma1: the carrier of ((0). c₁) = {(0. c₁)}
by RLSUB_1:def 3;

reconsider c₂ = [:the carrier of ((0). c₁),the carrier of ((0). c₁):] --> 0 as Function of [:the carrier of ((0). c₁),the carrier of ((0). c₁):], REAL by FUNCOP_1:57;

Lemma2: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . [b₁,b₂] = 0
by FUNCOP_1:13;

0. c₁ in the carrier of ((0). c₁)
by Lemma1, TARSKI:def 1;

then Lemma3: c₂ . [(0. c₁),(0. c₁)] = 0
by Lemma2;

Lemma4: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . [b₁,b₂] = c₂ . [b₂,b₁]

proof end;

Lemma5: for b₁, b₂, b₃ being VECTOR of ((0). c₁) holds c₂ . [(b₁ + b₂),b₃] = (c₂ . [b₁,b₃]) + (c₂ . [b₂,b₃])

proof end;

Lemma6: for b₁, b₂ being VECTOR of ((0). c₁)
for b₃ being Real holds c₂ . [(b₃ * b₁),b₂] = b₃ * (c₂ . [b₁,b₂])

proof end;

set c₃ = UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #);

E7: now

let c₄, c₅, c₆ be Point of UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #);
let c₇ be Real;
thus ( c₄ .|. c₄ = 0 iff c₄ = H₁( UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) )

proof

H₁( UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) = the Zero of UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)
.= 0. ((0). c₁)
.= 0. c₁ by RLSUB_1:19 ;
hence ( c₄ .|. c₄ = 0 iff c₄ = H₁( UNITSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #)) ) by Lemma1, Lemma3, TARSKI:def 1;

end;

thus 0 <= c₄ .|. c₄ by FUNCOP_1:13;
thus c₄ .|. c₅ = c₅ .|. c₄ by Lemma4;
thus (c₄ + c₅) .|. c₆ = (c₄ .|. c₆) + (c₅ .|. c₆)

proof

end;

thus (c₇ * c₄) .|. c₅ = c₇ * (c₄ .|. c₅)

proof

reconsider c₈ = c₄, c₉ = c₅ as VECTOR of ((0). c₁) ;
( (c₇ * c₄) .|. c₅ = c₂ . [(c₇ * c₈),c₉] & c₄ .|. c₅ = c₂ . [c₈,c₉] ) ;
hence (c₇ * c₄) .|. c₅ = c₇ * (c₄ .|. c₅) by Lemma6;

end;

definition

let c₄ be non empty UNITSTR ;
attr a₁ is RealUnitarySpace-like means :Def2: :: BHSP_1:def 2
for b₁, b₂, b₃ being Point of a₁
for b₄ being Real holds
( ( b₁ .|. b₁ = 0 implies b₁ = 0. a₁ ) & ( b₁ = 0. a₁ implies b₁ .|. b₁ = 0 ) & 0 <= b₁ .|. b₁ & b₁ .|. b₂ = b₂ .|. b₁ & (b₁ + b₂) .|. b₃ = (b₁ .|. b₃) + (b₂ .|. b₃) & (b₄ * b₁) .|. b₂ = b₄ * (b₁ .|. b₂) );

end;

:: deftheorem Def2 defines RealUnitarySpace-like BHSP_1:def 2 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict RealUnitarySpace-like UNITSTR ;
existence

proof end;

end;

definition

mode RealUnitarySpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealUnitarySpace-like UNITSTR ;

end;

definition

let c₄ be RealUnitarySpace;
let c₅, c₆ be Point of c₄;
redefine func .|. as c₂ .|. c₃ -> Real;
commutativity by Def2;

end;

theorem Th1: :: BHSP_1:1

canceled;

theorem Th2: :: BHSP_1:2

canceled;

theorem Th3: :: BHSP_1:3

canceled;

theorem Th4: :: BHSP_1:4

canceled;

theorem Th5: :: BHSP_1:5

canceled;

theorem Th6: :: BHSP_1:6

for b₁ being RealUnitarySpace holds (0. b₁) .|. (0. b₁) = 0 by Def2;

theorem Th7: :: BHSP_1:7

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds b₂ .|. (b₃ + b₄) = (b₂ .|. b₃) + (b₂ .|. b₄) by Def2;

theorem Th8: :: BHSP_1:8

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃, b₄ being Point of b₂ holds b₃ .|. (b₁ * b₄) = b₁ * (b₃ .|. b₄) by Def2;

theorem Th9: :: BHSP_1:9

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃, b₄ being Point of b₂ holds (b₁ * b₃) .|. b₄ = b₃ .|. (b₁ * b₄)

proof end;

theorem Th10: :: BHSP_1:10

for b₁, b₂ being Real
for b₃ being RealUnitarySpace
for b₄, b₅, b₆ being Point of b₃ holds ((b₁ * b₄) + (b₂ * b₅)) .|. b₆ = (b₁ * (b₄ .|. b₆)) + (b₂ * (b₅ .|. b₆))

proof end;

theorem Th11: :: BHSP_1:11

for b₁, b₂ being Real
for b₃ being RealUnitarySpace
for b₄, b₅, b₆ being Point of b₃ holds b₄ .|. ((b₁ * b₅) + (b₂ * b₆)) = (b₁ * (b₄ .|. b₅)) + (b₂ * (b₄ .|. b₆)) by Th10;

theorem Th12: :: BHSP_1:12

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. b₃ = b₂ .|. (- b₃)

proof end;

theorem Th13: :: BHSP_1:13

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. b₃ = - (b₂ .|. b₃)

proof end;

theorem Th14: :: BHSP_1:14

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds b₂ .|. (- b₃) = - (b₂ .|. b₃) by Th13;

theorem Th15: :: BHSP_1:15

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (- b₂) .|. (- b₃) = b₂ .|. b₃

proof end;

theorem Th16: :: BHSP_1:16

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds (b₂ - b₃) .|. b₄ = (b₂ .|. b₄) - (b₃ .|. b₄)

proof end;

theorem Th17: :: BHSP_1:17

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds b₂ .|. (b₃ - b₄) = (b₂ .|. b₃) - (b₂ .|. b₄)

proof end;

theorem Th18: :: BHSP_1:18

for b₁ being RealUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds (b₂ - b₃) .|. (b₄ - b₅) = (((b₂ .|. b₄) - (b₂ .|. b₅)) - (b₃ .|. b₄)) + (b₃ .|. b₅)

proof end;

theorem Th19: :: BHSP_1:19

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds (0. b₁) .|. b₂ = 0

proof end;

theorem Th20: :: BHSP_1:20

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds b₂ .|. (0. b₁) = 0 by Th19;

theorem Th21: :: BHSP_1:21

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ + b₃) .|. (b₂ + b₃) = ((b₂ .|. b₂) + (2 * (b₂ .|. b₃))) + (b₃ .|. b₃)

proof end;

theorem Th22: :: BHSP_1:22

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ + b₃) .|. (b₂ - b₃) = (b₂ .|. b₂) - (b₃ .|. b₃)

proof end;

theorem Th23: :: BHSP_1:23

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (b₂ - b₃) .|. (b₂ - b₃) = ((b₂ .|. b₂) - (2 * (b₂ .|. b₃))) + (b₃ .|. b₃)

proof end;

theorem Th24: :: BHSP_1:24

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds abs (b₂ .|. b₃) <= (sqrt (b₂ .|. b₂)) * (sqrt (b₃ .|. b₃))

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅, c₆ be Point of c₄;
pred c₂,c₃ are_orthogonal means :Def3: :: BHSP_1:def 3
a₂ .|. a₃ = 0;
symmetry ;

end;

:: deftheorem Def3 defines are_orthogonal BHSP_1:def 3 :

theorem Th25: :: BHSP_1:25

canceled;

theorem Th26: :: BHSP_1:26

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
b₂, - b₃ are_orthogonal

proof end;

theorem Th27: :: BHSP_1:27

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
- b₂,b₃ are_orthogonal

proof end;

theorem Th28: :: BHSP_1:28

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
- b₂, - b₃ are_orthogonal

proof end;

theorem Th29: :: BHSP_1:29

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds b₂, 0. b₁ are_orthogonal

proof end;

theorem Th30: :: BHSP_1:30

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
(b₂ + b₃) .|. (b₂ + b₃) = (b₂ .|. b₂) + (b₃ .|. b₃)

proof end;

theorem Th31: :: BHSP_1:31

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
(b₂ - b₃) .|. (b₂ - b₃) = (b₂ .|. b₂) + (b₃ .|. b₃)

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅ be Point of c₄;
func ||.c₂.|| -> Real equals :: BHSP_1:def 4
sqrt (a₂ .|. a₂);
correctness ;

end;

:: deftheorem Def4 defines ||. BHSP_1:def 4 :

theorem Th32: :: BHSP_1:32

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds
( ||.b₂.|| = 0 iff b₂ = 0. b₁ )

proof end;

theorem Th33: :: BHSP_1:33

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃ being Point of b₂ holds ||.(b₁ * b₃).|| = (abs b₁) * ||.b₃.||

proof end;

theorem Th34: :: BHSP_1:34

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds 0 <= ||.b₂.||

proof end;

theorem Th35: :: BHSP_1:35

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds abs (b₂ .|. b₃) <= ||.b₂.|| * ||.b₃.|| by Th24;

theorem Th36: :: BHSP_1:36

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ + b₃).|| <= ||.b₂.|| + ||.b₃.||

proof end;

theorem Th37: :: BHSP_1:37

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds ||.(- b₂).|| = ||.b₂.||

proof end;

theorem Th38: :: BHSP_1:38

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds ||.b₂.|| - ||.b₃.|| <= ||.(b₂ - b₃).||

proof end;

theorem Th39: :: BHSP_1:39

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds abs (||.b₂.|| - ||.b₃.||) <= ||.(b₂ - b₃).||

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅, c₆ be Point of c₄;
func dist c₂,c₃ -> Real equals :: BHSP_1:def 5
||.(a₂ - a₃).||;
correctness ;

end;

:: deftheorem Def5 defines dist BHSP_1:def 5 :

theorem Th40: :: BHSP_1:40

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ = dist b₃,b₂

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅, c₆ be Point of c₄;
redefine func dist as dist c₂,c₃ -> Real;
commutativity by Th40;

end;

theorem Th41: :: BHSP_1:41

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds dist b₂,b₂ = 0

proof end;

theorem Th42: :: BHSP_1:42

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist b₂,b₃ <= (dist b₂,b₄) + (dist b₄,b₃)

proof end;

theorem Th43: :: BHSP_1:43

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds
( b₂ <> b₃ iff dist b₂,b₃ <> 0 )

proof end;

theorem Th44: :: BHSP_1:44

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ >= 0 by Th34;

theorem Th45: :: BHSP_1:45

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds
( b₂ <> b₃ iff dist b₂,b₃ > 0 )

proof end;

theorem Th46: :: BHSP_1:46

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds dist b₂,b₃ = sqrt ((b₂ - b₃) .|. (b₂ - b₃)) ;

theorem Th47: :: BHSP_1:47

for b₁ being RealUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds dist (b₂ + b₃),(b₄ + b₅) <= (dist b₂,b₄) + (dist b₃,b₅)

proof end;

theorem Th48: :: BHSP_1:48

for b₁ being RealUnitarySpace
for b₂, b₃, b₄, b₅ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₅) <= (dist b₂,b₄) + (dist b₃,b₅)

proof end;

theorem Th49: :: BHSP_1:49

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₃) = dist b₂,b₄

proof end;

theorem Th50: :: BHSP_1:50

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being Point of b₁ holds dist (b₂ - b₃),(b₄ - b₃) <= (dist b₃,b₂) + (dist b₃,b₄)

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅ be sequence of c₄;
canceled;
canceled;
canceled;
canceled;
func - c₂ -> sequence of a₁ means :Def10: :: BHSP_1:def 10
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 BHSP_1:def 6 :

:: deftheorem Def7 BHSP_1:def 7 :

:: deftheorem Def8 BHSP_1:def 8 :

:: deftheorem Def9 BHSP_1:def 9 :

:: deftheorem Def10 defines - BHSP_1:def 10 :

definition

let c₄ be RealUnitarySpace;
let c₅ be sequence of c₄;
let c₆ be Point of c₄;
canceled;
func c₂ + c₃ -> sequence of a₁ means :Def12: :: BHSP_1:def 12
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 BHSP_1:def 11 :

:: deftheorem Def12 defines + BHSP_1:def 12 :

theorem Th51: :: BHSP_1:51

canceled;

theorem Th52: :: BHSP_1:52

canceled;

theorem Th53: :: BHSP_1:53

canceled;

theorem Th54: :: BHSP_1:54

canceled;

theorem Th55: :: BHSP_1:55

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

definition

let c₄ be RealUnitarySpace;
let c₅, c₆ be sequence of c₄;
redefine func + as c₂ + c₃ -> M6( NAT ,the carrier of a₁);
commutativity by Th55;

end;

theorem Th56: :: BHSP_1:56

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th57: :: BHSP_1:57

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is V45 & b₃ is V45 & b₄ = b₂ + b₃ holds
b₄ is V45

proof end;

theorem Th58: :: BHSP_1:58

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is V45 & b₃ is V45 & b₄ = b₂ - b₃ holds
b₄ is V45

proof end;

theorem Th59: :: BHSP_1:59

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃, b₄ being sequence of b₂ st b₃ is V45 & b₄ = b₁ * b₃ holds
b₄ is V45

proof end;

theorem Th60: :: BHSP_1:60

canceled;

theorem Th61: :: BHSP_1:61

canceled;

theorem Th62: :: BHSP_1:62

canceled;

theorem Th63: :: BHSP_1:63

canceled;

theorem Th64: :: BHSP_1:64

canceled;

theorem Th65: :: BHSP_1:65

canceled;

theorem Th66: :: BHSP_1:66

canceled;

theorem Th67: :: BHSP_1:67

canceled;

theorem Th68: :: BHSP_1:68

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V45 iff for b₃ being Nat holds b₂ . b₃ = b₂ . (b₃ + 1) )

proof end;

theorem Th69: :: BHSP_1:69

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V45 iff for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . (b₃ + b₄) )

proof end;

theorem Th70: :: BHSP_1:70

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is V45 iff for b₃, b₄ being Nat holds b₂ . b₃ = b₂ . b₄ )

proof end;

theorem Th71: :: BHSP_1:71

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th72: :: BHSP_1:72

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ = b₂ + (0. b₁)

proof end;

theorem Th73: :: BHSP_1:73

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃, b₄ being sequence of b₂ holds b₁ * (b₃ + b₄) = (b₁ * b₃) + (b₁ * b₄)

proof end;

theorem Th74: :: BHSP_1:74

for b₁, b₂ being Real
for b₃ being RealUnitarySpace
for b₄ being sequence of b₃ holds (b₁ + b₂) * b₄ = (b₁ * b₄) + (b₂ * b₄)

proof end;

theorem Th75: :: BHSP_1:75

for b₁, b₂ being Real
for b₃ being RealUnitarySpace
for b₄ being sequence of b₃ holds (b₁ * b₂) * b₄ = b₁ * (b₂ * b₄)

proof end;

theorem Th76: :: BHSP_1:76

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds 1 * b₂ = b₂

proof end;

theorem Th77: :: BHSP_1:77

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds (- 1) * b₂ = - b₂

proof end;

theorem Th78: :: BHSP_1:78

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ holds b₃ - b₂ = b₃ + (- b₂)

proof end;

theorem Th79: :: BHSP_1:79

for b₁ being RealUnitarySpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = - (b₃ - b₂)

proof end;

theorem Th80: :: BHSP_1:80

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ = b₂ - (0. b₁)

proof end;

theorem Th81: :: BHSP_1:81

for b₁ being RealUnitarySpace
for b₂ being sequence of b₁ holds b₂ = - (- b₂)

proof end;

theorem Th82: :: BHSP_1:82

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

theorem Th83: :: BHSP_1:83

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds (b₂ + b₃) - b₄ = b₂ + (b₃ - b₄)

proof end;

theorem Th84: :: BHSP_1:84

for b₁ being RealUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th85: :: BHSP_1:85

for b₁ being Real
for b₂ being RealUnitarySpace
for b₃, b₄ being sequence of b₂ holds b₁ * (b₃ - b₄) = (b₁ * b₃) - (b₁ * b₄)

proof end;