begin
theorem
for
x1,
y1,
z1,
x2,
y2,
z2 being ( ( ) (
V11()
real V116() )
Real) holds
|[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) )
+ |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V198() ) (
V47()
V73()
V141()
V142()
TopSpace-like V186()
V187()
V188()
V189()
V190()
V191()
V192()
V198() )
L16()) : ( ( ) ( )
set ) )
= |[(x1 : ( ( ) ( V11() real V116() ) Real) + x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(y1 : ( ( ) ( V11() real V116() ) Real) + y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(z1 : ( ( ) ( V11() real V116() ) Real) + z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) ;
theorem
for
x1,
y1,
z1,
x2,
y2,
z2 being ( ( ) (
V11()
real V116() )
Real) holds
|[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) )
- |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V198() ) (
V47()
V73()
V141()
V142()
TopSpace-like V186()
V187()
V188()
V189()
V190()
V191()
V192()
V198() )
L16()) : ( ( ) ( )
set ) )
= |[(x1 : ( ( ) ( V11() real V116() ) Real) - x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(y1 : ( ( ) ( V11() real V116() ) Real) - y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(z1 : ( ( ) ( V11() real V116() ) Real) - z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) ;
theorem
for
x1,
y1,
z1,
x2,
y2,
z2 being ( ( ) (
V11()
real V116() )
Real) holds
|[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) )
<X> |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) )
= |[((y1 : ( ( ) ( V11() real V116() ) Real) * z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (z1 : ( ( ) ( V11() real V116() ) Real) * y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((z1 : ( ( ) ( V11() real V116() ) Real) * x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (x1 : ( ( ) ( V11() real V116() ) Real) * z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((x1 : ( ( ) ( V11() real V116() ) Real) * y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (y1 : ( ( ) ( V11() real V116() ) Real) * x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) (
V13()
Function-like V41(3 : ( ( ) (
V1()
natural V11()
real V30()
V31()
V116()
V117()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( )
set ) ) ;