:: METRIC_4 semantic presentation

definition
let c1, c2 be non empty MetrSpace;
func dist_cart2S c1,c2 -> Function of [:[:the carrier of a1,the carrier of a2:],[:the carrier of a1,the carrier of a2:]:], REAL means :Def1: :: METRIC_4:def 1
for b1, b2 being Element of a1
for b3, b4 being Element of a2
for b5, b6 being Element of [:the carrier of a1,the carrier of a2:] st b5 = [b1,b3] & b6 = [b2,b4] holds
a3 . b5,b6 = sqrt (((dist b1,b2) ^2 ) + ((dist b3,b4) ^2 ));
existence
ex b1 being Function of [:[:the carrier of c1,the carrier of c2:],[:the carrier of c1,the carrier of c2:]:], REAL st
for b2, b3 being Element of c1
for b4, b5 being Element of c2
for b6, b7 being Element of [:the carrier of c1,the carrier of c2:] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = sqrt (((dist b2,b3) ^2 ) + ((dist b4,b5) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of c1,the carrier of c2:],[:the carrier of c1,the carrier of c2:]:], REAL st ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of [:the carrier of c1,the carrier of c2:] st b7 = [b3,b5] & b8 = [b4,b6] holds
b1 . b7,b8 = sqrt (((dist b3,b4) ^2 ) + ((dist b5,b6) ^2 )) ) & ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of [:the carrier of c1,the carrier of c2:] st b7 = [b3,b5] & b8 = [b4,b6] holds
b2 . b7,b8 = sqrt (((dist b3,b4) ^2 ) + ((dist b5,b6) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines dist_cart2S METRIC_4:def 1 :
for b1, b2 being non empty MetrSpace
for b3 being Function of [:[:the carrier of b1,the carrier of b2:],[:the carrier of b1,the carrier of b2:]:], REAL holds
( b3 = dist_cart2S b1,b2 iff for b4, b5 being Element of b1
for b6, b7 being Element of b2
for b8, b9 being Element of [:the carrier of b1,the carrier of b2:] st b8 = [b4,b6] & b9 = [b5,b7] holds
b3 . b8,b9 = sqrt (((dist b4,b5) ^2 ) + ((dist b6,b7) ^2 )) );

theorem Th1: :: METRIC_4:1
canceled;

theorem Th2: :: METRIC_4:2
for b1, b2 being real number st 0 <= b1 & 0 <= b2 holds
( sqrt (b1 + b2) = 0 iff ( b1 = 0 & b2 = 0 ) )
proof end;

theorem Th3: :: METRIC_4:3
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds
( (dist_cart2S b1,b2) . b3,b4 = 0 iff b3 = b4 )
proof end;

theorem Th4: :: METRIC_4:4
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds (dist_cart2S b1,b2) . b3,b4 = (dist_cart2S b1,b2) . b4,b3
proof end;

theorem Th5: :: METRIC_4:5
for b1, b2, b3, b4 being real number st 0 <= b1 & 0 <= b2 & 0 <= b3 & 0 <= b4 holds
sqrt (((b1 + b3) ^2 ) + ((b2 + b4) ^2 )) <= (sqrt ((b1 ^2 ) + (b2 ^2 ))) + (sqrt ((b3 ^2 ) + (b4 ^2 )))
proof end;

theorem Th6: :: METRIC_4:6
for b1, b2 being non empty MetrSpace
for b3, b4, b5 being Element of [:the carrier of b1,the carrier of b2:] holds (dist_cart2S b1,b2) . b3,b5 <= ((dist_cart2S b1,b2) . b3,b4) + ((dist_cart2S b1,b2) . b4,b5)
proof end;

definition
let c1, c2 be non empty MetrSpace;
let c3, c4 be Element of [:the carrier of c1,the carrier of c2:];
func dist2S c3,c4 -> Real equals :: METRIC_4:def 2
(dist_cart2S a1,a2) . a3,a4;
coherence
(dist_cart2S c1,c2) . c3,c4 is Real ;
end;

:: deftheorem Def2 defines dist2S METRIC_4:def 2 :
for b1, b2 being non empty MetrSpace
for b3, b4 being Element of [:the carrier of b1,the carrier of b2:] holds dist2S b3,b4 = (dist_cart2S b1,b2) . b3,b4;

definition
let c1, c2 be non empty MetrSpace;
func MetrSpaceCart2S c1,c2 -> non empty strict MetrSpace equals :: METRIC_4:def 3
 MetrStruct(# [:the carrier of a1,the carrier of a2:],(dist_cart2S a1,a2) #);
coherence
MetrStruct(# [:the carrier of c1,the carrier of c2:],(dist_cart2S c1,c2) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def3 defines MetrSpaceCart2S METRIC_4:def 3 :
for b1, b2 being non empty MetrSpace holds MetrSpaceCart2S b1,b2 = MetrStruct(# [:the carrier of b1,the carrier of b2:],(dist_cart2S b1,b2) #);

definition
let c1, c2, c3 be non empty MetrSpace;
func dist_cart3S c1,c2,c3 -> Function of [:[:the carrier of a1,the carrier of a2,the carrier of a3:],[:the carrier of a1,the carrier of a2,the carrier of a3:]:], REAL means :Def4: :: METRIC_4:def 4
for b1, b2 being Element of a1
for b3, b4 being Element of a2
for b5, b6 being Element of a3
for b7, b8 being Element of [:the carrier of a1,the carrier of a2,the carrier of a3:] st b7 = [b1,b3,b5] & b8 = [b2,b4,b6] holds
a4 . b7,b8 = sqrt ((((dist b1,b2) ^2 ) + ((dist b3,b4) ^2 )) + ((dist b5,b6) ^2 ));
existence
ex b1 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3:],[:the carrier of c1,the carrier of c2,the carrier of c3:]:], REAL st
for b2, b3 being Element of c1
for b4, b5 being Element of c2
for b6, b7 being Element of c3
for b8, b9 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = sqrt ((((dist b2,b3) ^2 ) + ((dist b4,b5) ^2 )) + ((dist b6,b7) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of c1,the carrier of c2,the carrier of c3:],[:the carrier of c1,the carrier of c2,the carrier of c3:]:], REAL st ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b1 . b9,b10 = sqrt ((((dist b3,b4) ^2 ) + ((dist b5,b6) ^2 )) + ((dist b7,b8) ^2 )) ) & ( for b3, b4 being Element of c1
for b5, b6 being Element of c2
for b7, b8 being Element of c3
for b9, b10 being Element of [:the carrier of c1,the carrier of c2,the carrier of c3:] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b2 . b9,b10 = sqrt ((((dist b3,b4) ^2 ) + ((dist b5,b6) ^2 )) + ((dist b7,b8) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist_cart3S METRIC_4:def 4 :
for b1, b2, b3 being non empty MetrSpace
for b4 being Function of [:[:the carrier of b1,the carrier of b2,the carrier of b3:],[:the carrier of b1,the carrier of b2,the carrier of b3:]:], REAL holds
( b4 = dist_cart3S b1,b2,b3 iff for b5, b6 being Element of b1
for b7, b8 being Element of b2
for b9, b10 being Element of b3
for b11, b12 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] st b11 = [b5,b7,b9] & b12 = [b6,b8,b10] holds
b4 . b11,b12 = sqrt ((((dist b5,b6) ^2 ) + ((dist b7,b8) ^2 )) + ((dist b9,b10) ^2 )) );

theorem Th7: :: METRIC_4:7
canceled;

theorem Th8: :: METRIC_4:8
canceled;

theorem Th9: :: METRIC_4:9
canceled;

theorem Th10: :: METRIC_4:10
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds
( (dist_cart3S b1,b2,b3) . b4,b5 = 0 iff b4 = b5 )
proof end;

theorem Th11: :: METRIC_4:11
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds (dist_cart3S b1,b2,b3) . b4,b5 = (dist_cart3S b1,b2,b3) . b5,b4
proof end;

theorem Th12: :: METRIC_4:12
for b1, b2, b3 being complex number holds ((b1 + b2) + b3) ^2 = (((b1 ^2 ) + (b2 ^2 )) + (b3 ^2 )) + ((((2 * b1) * b2) + ((2 * b1) * b3)) + ((2 * b2) * b3))
proof end;

theorem Th13: :: METRIC_4:13
for b1, b2, b3, b4, b5, b6 being real number holds (((2 * (b1 * b4)) * (b3 * b2)) + ((2 * (b1 * b6)) * (b5 * b3))) + ((2 * (b2 * b6)) * (b5 * b4)) <= ((((((b1 * b4) ^2 ) + ((b3 * b2) ^2 )) + ((b1 * b6) ^2 )) + ((b5 * b3) ^2 )) + ((b2 * b6) ^2 )) + ((b5 * b4) ^2 )
proof end;

theorem Th14: :: METRIC_4:14
canceled;

theorem Th15: :: METRIC_4:15
for b1, b2, b3, b4, b5, b6 being real number holds (((b1 * b3) + (b2 * b4)) + (b5 * b6)) ^2 <= (((b1 ^2 ) + (b2 ^2 )) + (b5 ^2 )) * (((b3 ^2 ) + (b4 ^2 )) + (b6 ^2 ))
proof end;

Lemma13: for b1, b2, b3, b4, b5, b6 being real number st 0 <= b1 & 0 <= b2 & 0 <= b3 & 0 <= b4 & 0 <= b5 & 0 <= b6 holds
sqrt ((((b1 + b3) ^2 ) + ((b2 + b4) ^2 )) + ((b5 + b6) ^2 )) <= (sqrt (((b1 ^2 ) + (b2 ^2 )) + (b5 ^2 ))) + (sqrt (((b3 ^2 ) + (b4 ^2 )) + (b6 ^2 )))
proof end;

theorem Th16: :: METRIC_4:16
for b1, b2, b3 being non empty MetrSpace
for b4, b5, b6 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds (dist_cart3S b1,b2,b3) . b4,b6 <= ((dist_cart3S b1,b2,b3) . b4,b5) + ((dist_cart3S b1,b2,b3) . b5,b6)
proof end;

definition
let c1, c2, c3 be non empty MetrSpace;
let c4, c5 be Element of [:the carrier of c1,the carrier of c2,the carrier of c3:];
func dist3S c4,c5 -> Real equals :: METRIC_4:def 5
(dist_cart3S a1,a2,a3) . a4,a5;
coherence
(dist_cart3S c1,c2,c3) . c4,c5 is Real ;
end;

:: deftheorem Def5 defines dist3S METRIC_4:def 5 :
for b1, b2, b3 being non empty MetrSpace
for b4, b5 being Element of [:the carrier of b1,the carrier of b2,the carrier of b3:] holds dist3S b4,b5 = (dist_cart3S b1,b2,b3) . b4,b5;

definition
let c1, c2, c3 be non empty MetrSpace;
func MetrSpaceCart3S c1,c2,c3 -> non empty strict MetrSpace equals :: METRIC_4:def 6
 MetrStruct(# [:the carrier of a1,the carrier of a2,the carrier of a3:],(dist_cart3S a1,a2,a3) #);
coherence
MetrStruct(# [:the carrier of c1,the carrier of c2,the carrier of c3:],(dist_cart3S c1,c2,c3) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def6 defines MetrSpaceCart3S METRIC_4:def 6 :
for b1, b2, b3 being non empty MetrSpace holds MetrSpaceCart3S b1,b2,b3 = MetrStruct(# [:the carrier of b1,the carrier of b2,the carrier of b3:],(dist_cart3S b1,b2,b3) #);

theorem Th17: :: METRIC_4:17
canceled;

theorem Th18: :: METRIC_4:18
canceled;

definition
func taxi_dist2 -> Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL means :Def7: :: METRIC_4:def 7
for b1, b2, b3, b4 being Element of REAL
for b5, b6 being Element of [:REAL ,REAL :] st b5 = [b1,b3] & b6 = [b2,b4] holds
a1 . b5,b6 = (real_dist . b1,b2) + (real_dist . b3,b4);
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st
for b2, b3, b4, b5 being Element of REAL
for b6, b7 being Element of [:REAL ,REAL :] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = (real_dist . b2,b3) + (real_dist . b4,b5)
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st ( for b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL :] st b7 = [b3,b5] & b8 = [b4,b6] holds
b1 . b7,b8 = (real_dist . b3,b4) + (real_dist . b5,b6) ) & ( for b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL :] st b7 = [b3,b5] & b8 = [b4,b6] holds
b2 . b7,b8 = (real_dist . b3,b4) + (real_dist . b5,b6) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines taxi_dist2 METRIC_4:def 7 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL holds
( b1 = taxi_dist2 iff for b2, b3, b4, b5 being Element of REAL
for b6, b7 being Element of [:REAL ,REAL :] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = (real_dist . b2,b3) + (real_dist . b4,b5) );

theorem Th19: :: METRIC_4:19
for b1, b2 being Element of [:REAL ,REAL :] holds
( taxi_dist2 . b1,b2 = 0 iff b1 = b2 )
proof end;

theorem Th20: :: METRIC_4:20
for b1, b2 being Element of [:REAL ,REAL :] holds taxi_dist2 . b1,b2 = taxi_dist2 . b2,b1
proof end;

theorem Th21: :: METRIC_4:21
for b1, b2, b3 being Element of [:REAL ,REAL :] holds taxi_dist2 . b1,b3 <= (taxi_dist2 . b1,b2) + (taxi_dist2 . b2,b3)
proof end;

definition
func RealSpaceCart2 -> non empty strict MetrSpace equals :: METRIC_4:def 8
 MetrStruct(# [:REAL ,REAL :],taxi_dist2 #);
coherence
MetrStruct(# [:REAL ,REAL :],taxi_dist2 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def8 defines RealSpaceCart2 METRIC_4:def 8 :
RealSpaceCart2 = MetrStruct(# [:REAL ,REAL :],taxi_dist2 #);

definition
func Eukl_dist2 -> Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL means :Def9: :: METRIC_4:def 9
for b1, b2, b3, b4 being Element of REAL
for b5, b6 being Element of [:REAL ,REAL :] st b5 = [b1,b3] & b6 = [b2,b4] holds
a1 . b5,b6 = sqrt (((real_dist . b1,b2) ^2 ) + ((real_dist . b3,b4) ^2 ));
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st
for b2, b3, b4, b5 being Element of REAL
for b6, b7 being Element of [:REAL ,REAL :] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = sqrt (((real_dist . b2,b3) ^2 ) + ((real_dist . b4,b5) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st ( for b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL :] st b7 = [b3,b5] & b8 = [b4,b6] holds
b1 . b7,b8 = sqrt (((real_dist . b3,b4) ^2 ) + ((real_dist . b5,b6) ^2 )) ) & ( for b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL :] st b7 = [b3,b5] & b8 = [b4,b6] holds
b2 . b7,b8 = sqrt (((real_dist . b3,b4) ^2 ) + ((real_dist . b5,b6) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Eukl_dist2 METRIC_4:def 9 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL holds
( b1 = Eukl_dist2 iff for b2, b3, b4, b5 being Element of REAL
for b6, b7 being Element of [:REAL ,REAL :] st b6 = [b2,b4] & b7 = [b3,b5] holds
b1 . b6,b7 = sqrt (((real_dist . b2,b3) ^2 ) + ((real_dist . b4,b5) ^2 )) );

theorem Th22: :: METRIC_4:22
for b1, b2 being Element of [:REAL ,REAL :] holds
( Eukl_dist2 . b1,b2 = 0 iff b1 = b2 )
proof end;

theorem Th23: :: METRIC_4:23
for b1, b2 being Element of [:REAL ,REAL :] holds Eukl_dist2 . b1,b2 = Eukl_dist2 . b2,b1
proof end;

theorem Th24: :: METRIC_4:24
for b1, b2, b3 being Element of [:REAL ,REAL :] holds Eukl_dist2 . b1,b3 <= (Eukl_dist2 . b1,b2) + (Eukl_dist2 . b2,b3)
proof end;

definition
func EuklSpace2 -> non empty strict MetrSpace equals :: METRIC_4:def 10
 MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #);
coherence
MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def10 defines EuklSpace2 METRIC_4:def 10 :
EuklSpace2 = MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #);

definition
func taxi_dist3 -> Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL means :Def11: :: METRIC_4:def 11
for b1, b2, b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL ,REAL :] st b7 = [b1,b3,b5] & b8 = [b2,b4,b6] holds
a1 . b7,b8 = ((real_dist . b1,b2) + (real_dist . b3,b4)) + (real_dist . b5,b6);
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st
for b2, b3, b4, b5, b6, b7 being Element of REAL
for b8, b9 being Element of [:REAL ,REAL ,REAL :] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = ((real_dist . b2,b3) + (real_dist . b4,b5)) + (real_dist . b6,b7)
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st ( for b3, b4, b5, b6, b7, b8 being Element of REAL
for b9, b10 being Element of [:REAL ,REAL ,REAL :] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b1 . b9,b10 = ((real_dist . b3,b4) + (real_dist . b5,b6)) + (real_dist . b7,b8) ) & ( for b3, b4, b5, b6, b7, b8 being Element of REAL
for b9, b10 being Element of [:REAL ,REAL ,REAL :] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b2 . b9,b10 = ((real_dist . b3,b4) + (real_dist . b5,b6)) + (real_dist . b7,b8) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines taxi_dist3 METRIC_4:def 11 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL holds
( b1 = taxi_dist3 iff for b2, b3, b4, b5, b6, b7 being Element of REAL
for b8, b9 being Element of [:REAL ,REAL ,REAL :] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = ((real_dist . b2,b3) + (real_dist . b4,b5)) + (real_dist . b6,b7) );

theorem Th25: :: METRIC_4:25
for b1, b2 being Element of [:REAL ,REAL ,REAL :] holds
( taxi_dist3 . b1,b2 = 0 iff b1 = b2 )
proof end;

theorem Th26: :: METRIC_4:26
for b1, b2 being Element of [:REAL ,REAL ,REAL :] holds taxi_dist3 . b1,b2 = taxi_dist3 . b2,b1
proof end;

theorem Th27: :: METRIC_4:27
for b1, b2, b3 being Element of [:REAL ,REAL ,REAL :] holds taxi_dist3 . b1,b3 <= (taxi_dist3 . b1,b2) + (taxi_dist3 . b2,b3)
proof end;

definition
func RealSpaceCart3 -> non empty strict MetrSpace equals :: METRIC_4:def 12
 MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #);
coherence
MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def12 defines RealSpaceCart3 METRIC_4:def 12 :
RealSpaceCart3 = MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #);

definition
func Eukl_dist3 -> Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL means :Def13: :: METRIC_4:def 13
for b1, b2, b3, b4, b5, b6 being Element of REAL
for b7, b8 being Element of [:REAL ,REAL ,REAL :] st b7 = [b1,b3,b5] & b8 = [b2,b4,b6] holds
a1 . b7,b8 = sqrt ((((real_dist . b1,b2) ^2 ) + ((real_dist . b3,b4) ^2 )) + ((real_dist . b5,b6) ^2 ));
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st
for b2, b3, b4, b5, b6, b7 being Element of REAL
for b8, b9 being Element of [:REAL ,REAL ,REAL :] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = sqrt ((((real_dist . b2,b3) ^2 ) + ((real_dist . b4,b5) ^2 )) + ((real_dist . b6,b7) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st ( for b3, b4, b5, b6, b7, b8 being Element of REAL
for b9, b10 being Element of [:REAL ,REAL ,REAL :] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b1 . b9,b10 = sqrt ((((real_dist . b3,b4) ^2 ) + ((real_dist . b5,b6) ^2 )) + ((real_dist . b7,b8) ^2 )) ) & ( for b3, b4, b5, b6, b7, b8 being Element of REAL
for b9, b10 being Element of [:REAL ,REAL ,REAL :] st b9 = [b3,b5,b7] & b10 = [b4,b6,b8] holds
b2 . b9,b10 = sqrt ((((real_dist . b3,b4) ^2 ) + ((real_dist . b5,b6) ^2 )) + ((real_dist . b7,b8) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Eukl_dist3 METRIC_4:def 13 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL holds
( b1 = Eukl_dist3 iff for b2, b3, b4, b5, b6, b7 being Element of REAL
for b8, b9 being Element of [:REAL ,REAL ,REAL :] st b8 = [b2,b4,b6] & b9 = [b3,b5,b7] holds
b1 . b8,b9 = sqrt ((((real_dist . b2,b3) ^2 ) + ((real_dist . b4,b5) ^2 )) + ((real_dist . b6,b7) ^2 )) );

theorem Th28: :: METRIC_4:28
for b1, b2 being Element of [:REAL ,REAL ,REAL :] holds
( Eukl_dist3 . b1,b2 = 0 iff b1 = b2 )
proof end;

theorem Th29: :: METRIC_4:29
for b1, b2 being Element of [:REAL ,REAL ,REAL :] holds Eukl_dist3 . b1,b2 = Eukl_dist3 . b2,b1
proof end;

theorem Th30: :: METRIC_4:30
for b1, b2, b3 being Element of [:REAL ,REAL ,REAL :] holds Eukl_dist3 . b1,b3 <= (Eukl_dist3 . b1,b2) + (Eukl_dist3 . b2,b3)
proof end;

definition
func EuklSpace3 -> non empty strict MetrSpace equals :: METRIC_4:def 14
 MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #);
coherence
MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem Def14 defines EuklSpace3 METRIC_4:def 14 :
EuklSpace3 = MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #);