:: PDIFF_4 semantic presentation

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(