REAL is V1() V54() V160() V161() V162() V166() set
NAT is V1() epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V54() V160() V166() set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
omega is V1() epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
RAT is V1() V54() V160() V161() V162() V163() V166() set
INT is V1() V54() V160() V161() V162() V163() V164() V166() set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
K7(1,1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
K7(2,2) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V66() V92() V117() V118() V119() V120() V121() V122() V123() V172() V202() V210() L20()
the U1 of (TOP-REAL 2) is set
REAL 1 is V1() functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
K418(1) is V66() V129() L15()
the U1 of K418(1) is set
K279(K418(1),K418(1)) is V66() L15()
the U1 of K279(K418(1),K418(1)) is set
REAL 2 is V1() functional FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 2),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((REAL 2),REAL)) is set
3 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL 3 is V1() functional FinSequence-membered FinSequenceSet of REAL
3 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL 3)) is set
K6(K7(REAL,(REAL 3))) is set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
K552() is V66() V94() L8()
the U1 of K552() is set
K557() is V66() L8()
K558() is V66() V94() M15(K557())
K559() is V66() V94() V137() V225() M18(K557(),K558())
K561() is V66() V94() V137() V139() V141() L8()
K562() is V66() V94() V137() V225() M15(K561())
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
the V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered V160() V161() V162() V163() V164() V165() V166() set is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered V160() V161() V162() V163() V164() V165() V166() set
0c is set
K7((REAL 3),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((REAL 3),REAL)) is set
proj (1,3) is V1() V16() V19( REAL 3) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom (proj (1,3)) is functional FinSequence-membered Element of K6((REAL 3))
K6((REAL 3)) is set
rng (proj (1,3)) is V160() V161() V162() Element of K6(REAL)
f1 is set
the V11() real ext-real Element of REAL is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*f2, the V11() real ext-real Element of REAL , the V11() real ext-real Element of REAL *> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
(proj (1,3)) . g1 is V11() real ext-real Element of REAL
g1 . 1 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (1,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
<*f1,f2,f3*> . 1 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (1,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
proj (2,3) is V1() V16() V19( REAL 3) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom (proj (2,3)) is functional FinSequence-membered Element of K6((REAL 3))
rng (proj (2,3)) is V160() V161() V162() Element of K6(REAL)
f1 is set
the V11() real ext-real Element of REAL is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<* the V11() real ext-real Element of REAL ,f2, the V11() real ext-real Element of REAL *> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
(proj (2,3)) . g1 is V11() real ext-real Element of REAL
g1 . 2 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (2,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
<*f1,f2,f3*> . 2 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (2,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
proj (3,3) is V1() V16() V19( REAL 3) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom (proj (3,3)) is functional FinSequence-membered Element of K6((REAL 3))
rng (proj (3,3)) is V160() V161() V162() Element of K6(REAL)
f1 is set
the V11() real ext-real Element of REAL is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<* the V11() real ext-real Element of REAL , the V11() real ext-real Element of REAL ,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
(proj (3,3)) . g1 is V11() real ext-real Element of REAL
g1 . 3 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (3,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
<*f1,f2,f3*> . 3 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f1,f2,f3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (3,3)) . <*f1,f2,f3*> is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (1,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,3)) . f3 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (2,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,3)) . f3 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (3,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (3,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (3,3)) . f3 is V11() real ext-real Element of REAL
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (1,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (1,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (1,3)) . f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (2,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (2,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (2,3)) . f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (3,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (3,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(proj (3,3)) . f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (1,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,g1,f3)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (1,g1,f3)) . p is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
<*g2,g3,z*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (2,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,g1,f3)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (2,g1,f3)) . f1 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
<*g2,g3,z*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (3,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (3,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (3,g1,f3)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (3,g1,f3)) . f2 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
<*g2,g3,z*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (1,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (1,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,p,f1)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (1,p,f1)) . f2 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of f2
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g2 is open V160() V161() V162() Neighbourhood of f2
(SVF1 (1,p,f1)) . f2 is V11() real ext-real Element of REAL
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (1,p,f1)) . f2 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of f2
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g2 is open V160() V161() V162() Neighbourhood of f2
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g3 is open V160() V161() V162() Neighbourhood of f2
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (2,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (2,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,p,f1)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (2,p,f1)) . f3 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of f3
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f3 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g2 is open V160() V161() V162() Neighbourhood of f3
(SVF1 (2,p,f1)) . f3 is V11() real ext-real Element of REAL
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (2,p,f1)) . f3 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of f3
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g2 is open V160() V161() V162() Neighbourhood of f3
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g3 is open V160() V161() V162() Neighbourhood of f3
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (3,p,f1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,f1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (3,f1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (3,p,f1)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (3,p,f1)) . g1 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of g1
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g2 is open V160() V161() V162() Neighbourhood of g1
(SVF1 (3,p,f1)) . g1 is V11() real ext-real Element of REAL
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f2 is V11() real ext-real Element of REAL
f3 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
<*f2,f3,g1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (3,p,f1)) . g1 is V11() real ext-real Element of REAL
g2 is open V160() V161() V162() Neighbourhood of g1
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g2 is open V160() V161() V162() Neighbourhood of g1
g3 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
g3 is open V160() V161() V162() Neighbourhood of g1
z is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (1,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (1,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,g2,g1)),p) is V11() real ext-real Element of REAL
dom (SVF1 (1,g2,g1)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (1,g2,g1)) . p is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of p
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 . 1 is V11() real ext-real Element of REAL
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
<*z,R1,x1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (1,g2,g1)) . z is V11() real ext-real Element of REAL
y1 is open V160() V161() V162() Neighbourhood of z
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of z
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (2,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (2,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,g2,g1)),f1) is V11() real ext-real Element of REAL
dom (SVF1 (2,g2,g1)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (2,g2,g1)) . f1 is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of f1
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 . 1 is V11() real ext-real Element of REAL
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
<*z,R1,x1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (2,g2,g1)) . R1 is V11() real ext-real Element of REAL
y1 is open V160() V161() V162() Neighbourhood of R1
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of R1
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
SVF1 (3,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (3,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (3,g2,g1)),f2) is V11() real ext-real Element of REAL
dom (SVF1 (3,g2,g1)) is V160() V161() V162() Element of K6(REAL)
(SVF1 (3,g2,g1)) . f2 is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of f2
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 . 1 is V11() real ext-real Element of REAL
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
<*z,R1,x1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (3,g2,g1)) . x1 is V11() real ext-real Element of REAL
y1 is open V160() V161() V162() Neighbourhood of x1
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of x1
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
z1 . 1 is V11() real ext-real Element of REAL
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g2,g1,1) is V11() real ext-real Element of REAL
reproj (1,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (1,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,3)) . g1 is V11() real ext-real Element of REAL
diff ((g2 * (reproj (1,g1))),((proj (1,3)) . g1)) is V11() real ext-real Element of REAL
SVF1 (1,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,g2,g1)) is V160() V161() V162() Element of K6(REAL)
diff ((SVF1 (1,g2,g1)),p) is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
<*g3,z,R1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (1,g2,g1)) . g3 is V11() real ext-real Element of REAL
x1 is open V160() V161() V162() Neighbourhood of g3
y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y1 . 1 is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g2,g1,2) is V11() real ext-real Element of REAL
reproj (2,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (2,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,3)) . g1 is V11() real ext-real Element of REAL
diff ((g2 * (reproj (2,g1))),((proj (2,3)) . g1)) is V11() real ext-real Element of REAL
SVF1 (2,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,g2,g1)) is V160() V161() V162() Element of K6(REAL)
diff ((SVF1 (2,g2,g1)),f1) is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
<*g3,z,R1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (2,g2,g1)) . z is V11() real ext-real Element of REAL
x1 is open V160() V161() V162() Neighbourhood of z
y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y1 . 1 is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
f3 is V11() real ext-real Element of REAL
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
g2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g2,g1,3) is V11() real ext-real Element of REAL
reproj (3,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g2 * (reproj (3,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (3,3)) . g1 is V11() real ext-real Element of REAL
diff ((g2 * (reproj (3,g1))),((proj (3,3)) . g1)) is V11() real ext-real Element of REAL
SVF1 (3,g2,g1) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (3,g2,g1)) is V160() V161() V162() Element of K6(REAL)
diff ((SVF1 (3,g2,g1)),f2) is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
R1 is V11() real ext-real Element of REAL
<*g3,z,R1*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (3,g2,g1)) . R1 is V11() real ext-real Element of REAL
x1 is open V160() V161() V162() Neighbourhood of R1
y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y1 . 1 is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g1,f3,1) is V11() real ext-real Element of REAL
reproj (1,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,3)) . f3 is V11() real ext-real Element of REAL
diff ((g1 * (reproj (1,f3))),((proj (1,3)) . f3)) is V11() real ext-real Element of REAL
SVF1 (1,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,g1,f3)),p) is V11() real ext-real Element of REAL
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g1,f3,2) is V11() real ext-real Element of REAL
reproj (2,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,3)) . f3 is V11() real ext-real Element of REAL
diff ((g1 * (reproj (2,f3))),((proj (2,3)) . f3)) is V11() real ext-real Element of REAL
SVF1 (2,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,g1,f3)),f1) is V11() real ext-real Element of REAL
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
p is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*p,f1,f2*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
g1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
partdiff (g1,f3,3) is V11() real ext-real Element of REAL
reproj (3,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
g1 * (reproj (3,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (3,3)) . f3 is V11() real ext-real Element of REAL
diff ((g1 * (reproj (3,f3))),((proj (3,3)) . f3)) is V11() real ext-real Element of REAL
SVF1 (3,g1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (3,g1,f3)),f2) is V11() real ext-real Element of REAL
p is set
f1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f1 is functional FinSequence-membered Element of K6((REAL 3))
f1 | p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (1,(f1 | p),f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
(f1 | p) * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(f1 | p),f3)) is V160() V161() V162() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
<*g1,g2,g3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (1,(f1 | p),f3)) . g1 is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of g1
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is open V160() V161() V162() Neighbourhood of g1
SVF1 (1,f1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f1 * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,f1,f3)) is V160() V161() V162() Element of K6(REAL)
R1 is V11() real ext-real Element of REAL
dom (reproj (1,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (1,f3)) . R1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(dom f1) /\ p is functional FinSequence-membered Element of K6((REAL 3))
R1 is set
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
(SVF1 (1,f1,f3)) . g1 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
(SVF1 (1,f1,f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (1,f1,f3)) . y1) - ((SVF1 (1,f1,f3)) . g1) is V11() real ext-real Element of REAL
y1 - g1 is V11() real ext-real Element of REAL
R1 . (y1 - g1) is V11() real ext-real Element of REAL
x1 . (y1 - g1) is V11() real ext-real Element of REAL
(R1 . (y1 - g1)) + (x1 . (y1 - g1)) is V11() real ext-real Element of REAL
z1 is V11() real ext-real Element of REAL
(SVF1 (1,(f1 | p),f3)) . z1 is V11() real ext-real Element of REAL
(SVF1 (1,f1,f3)) . z1 is V11() real ext-real Element of REAL
dom (reproj (1,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (1,f3)) . z1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(f1 | p) . ((reproj (1,f3)) . z1) is V11() real ext-real Element of REAL
f1 . ((reproj (1,f3)) . z1) is V11() real ext-real Element of REAL
(SVF1 (1,(f1 | p),f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (1,(f1 | p),f3)) . y1) - ((SVF1 (1,(f1 | p),f3)) . g1) is V11() real ext-real Element of REAL
((SVF1 (1,f1,f3)) . y1) - ((SVF1 (1,(f1 | p),f3)) . g1) is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of g1
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is set
f1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f1 is functional FinSequence-membered Element of K6((REAL 3))
f1 | p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (2,(f1 | p),f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
(f1 | p) * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(f1 | p),f3)) is V160() V161() V162() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
<*g1,g2,g3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (2,(f1 | p),f3)) . g2 is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of g2
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is open V160() V161() V162() Neighbourhood of g2
SVF1 (2,f1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f1 * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,f1,f3)) is V160() V161() V162() Element of K6(REAL)
R1 is V11() real ext-real Element of REAL
dom (reproj (2,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (2,f3)) . R1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(dom f1) /\ p is functional FinSequence-membered Element of K6((REAL 3))
R1 is set
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
(SVF1 (2,f1,f3)) . g2 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
(SVF1 (2,f1,f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (2,f1,f3)) . y1) - ((SVF1 (2,f1,f3)) . g2) is V11() real ext-real Element of REAL
y1 - g2 is V11() real ext-real Element of REAL
R1 . (y1 - g2) is V11() real ext-real Element of REAL
x1 . (y1 - g2) is V11() real ext-real Element of REAL
(R1 . (y1 - g2)) + (x1 . (y1 - g2)) is V11() real ext-real Element of REAL
z1 is V11() real ext-real Element of REAL
(SVF1 (2,(f1 | p),f3)) . z1 is V11() real ext-real Element of REAL
(SVF1 (2,f1,f3)) . z1 is V11() real ext-real Element of REAL
dom (reproj (2,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (2,f3)) . z1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(f1 | p) . ((reproj (2,f3)) . z1) is V11() real ext-real Element of REAL
f1 . ((reproj (2,f3)) . z1) is V11() real ext-real Element of REAL
(SVF1 (2,(f1 | p),f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (2,(f1 | p),f3)) . y1) - ((SVF1 (2,(f1 | p),f3)) . g2) is V11() real ext-real Element of REAL
((SVF1 (2,f1,f3)) . y1) - ((SVF1 (2,(f1 | p),f3)) . g2) is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of g2
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is set
f1 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f1 is functional FinSequence-membered Element of K6((REAL 3))
f1 | p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
SVF1 (3,(f1 | p),f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (3,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
(f1 | p) * (reproj (3,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (3,(f1 | p),f3)) is V160() V161() V162() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
g2 is V11() real ext-real Element of REAL
g3 is V11() real ext-real Element of REAL
<*g1,g2,g3*> is V1() V16() V19( NAT ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like set
(SVF1 (3,(f1 | p),f3)) . g3 is V11() real ext-real Element of REAL
z is open V160() V161() V162() Neighbourhood of g3
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z is open V160() V161() V162() Neighbourhood of g3
SVF1 (3,f1,f3) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f1 * (reproj (3,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (3,f1,f3)) is V160() V161() V162() Element of K6(REAL)
R1 is V11() real ext-real Element of REAL
dom (reproj (3,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (3,f3)) . R1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(dom f1) /\ p is functional FinSequence-membered Element of K6((REAL 3))
R1 is set
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
(SVF1 (3,f1,f3)) . g3 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
(SVF1 (3,f1,f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (3,f1,f3)) . y1) - ((SVF1 (3,f1,f3)) . g3) is V11() real ext-real Element of REAL
y1 - g3 is V11() real ext-real Element of REAL
R1 . (y1 - g3) is V11() real ext-real Element of REAL
x1 . (y1 - g3) is V11() real ext-real Element of REAL
(R1 . (y1 - g3)) + (x1 . (y1 - g3)) is V11() real ext-real Element of REAL
z1 is V11() real ext-real Element of REAL
(SVF1 (3,(f1 | p),f3)) . z1 is V11() real ext-real Element of REAL
(SVF1 (3,f1,f3)) . z1 is V11() real ext-real Element of REAL
dom (reproj (3,f3)) is V160() V161() V162() Element of K6(REAL)
(reproj (3,f3)) . z1 is V16() V19( NAT ) Function-like V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
dom (f1 | p) is functional FinSequence-membered Element of K6((REAL 3))
(f1 | p) . ((reproj (3,f3)) . z1) is V11() real ext-real Element of REAL
f1 . ((reproj (3,f3)) . z1) is V11() real ext-real Element of REAL
(SVF1 (3,(f1 | p),f3)) . y1 is V11() real ext-real Element of REAL
((SVF1 (3,(f1 | p),f3)) . y1) - ((SVF1 (3,(f1 | p),f3)) . g3) is V11() real ext-real Element of REAL
((SVF1 (3,f1,f3)) . y1) - ((SVF1 (3,(f1 | p),f3)) . g3) is V11() real ext-real Element of REAL
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y1 is open V160() V161() V162() Neighbourhood of g3
z1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is set
f2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f2 is functional FinSequence-membered Element of K6((REAL 3))
f3 is set
f3 is set
dom p is functional FinSequence-membered Element of K6((REAL 3))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
f2 . f3 is V11() real ext-real Element of REAL
partdiff (p,f3,1) is V11() real ext-real Element of REAL
reproj (1,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (1,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,3)) . f3 is V11() real ext-real Element of REAL
diff ((p * (reproj (1,f3))),((proj (1,3)) . f3)) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f2 is functional FinSequence-membered Element of K6((REAL 3))
f3 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f3 is functional FinSequence-membered Element of K6((REAL 3))
g1 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
f2 . g1 is V11() real ext-real Element of REAL
partdiff (p,g1,1) is V11() real ext-real Element of REAL
reproj (1,g1) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (1,g1)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,3)) . g1 is V11() real ext-real Element of REAL
diff ((p * (reproj (1,g1))),((proj (1,3)) . g1)) is V11() real ext-real Element of REAL
f3 . g1 is V11() real ext-real Element of REAL
p is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
f1 is set
f2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f2 is functional FinSequence-membered Element of K6((REAL 3))
f3 is set
f3 is set
dom p is functional FinSequence-membered Element of K6((REAL 3))
f3 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(3) FinSequence-like FinSubsequence-like Element of REAL 3
f2 . f3 is V11() real ext-real Element of REAL
partdiff (p,f3,2) is V11() real ext-real Element of REAL
reproj (2,f3) is V1() V16() V19( REAL ) V20( REAL 3) Function-like total quasi_total V134() V135() Element of K6(K7(REAL,(REAL 3)))
p * (reproj (2,f3)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,3)) . f3 is V11() real ext-real Element of REAL
diff ((p * (reproj (2,f3))),((proj (2,3)) . f3)) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 3) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))
dom f2 is functional FinSequence-membered Element of K6((REAL 3))
f3 is V16() V19(