:: by Jaros{\l}aw Kotowicz

::

:: Received September 21, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th2: :: SCHEME1:2

for n being Element of NAT ex m being Element of NAT st

( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 )

( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 )

proof end;

theorem Th3: :: SCHEME1:3

for n being Element of NAT ex m being Element of NAT st

( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 )

( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 )

proof end;

theorem Th4: :: SCHEME1:4

for n being Element of NAT ex m being Element of NAT st

( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 )

( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 )

proof end;

scheme :: SCHEME1:sch 1

ExRealSubseq{ F_{1}() -> Real_Sequence, P_{1}[ object ] } :

ExRealSubseq{ F

ex q being Real_Sequence st

( q is subsequence of F_{1}() & ( for n being Nat holds P_{1}[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) holds

ex m being Element of NAT st F_{1}() . n = q . m ) )

provided
( q is subsequence of F

P

ex m being Element of NAT st F

proof end;

scheme :: SCHEME1:sch 4

ExRealSeq4{ F_{1}( set ) -> Element of REAL , F_{2}( set ) -> Element of REAL , F_{3}( set ) -> Element of REAL , F_{4}( set ) -> Element of REAL } :

ExRealSeq4{ F

ex s being Real_Sequence st

for n being Element of NAT holds

( s . (4 * n) = F_{1}(n) & s . ((4 * n) + 1) = F_{2}(n) & s . ((4 * n) + 2) = F_{3}(n) & s . ((4 * n) + 3) = F_{4}(n) )

for n being Element of NAT holds

( s . (4 * n) = F

proof end;

scheme :: SCHEME1:sch 5

ExRealSeq5{ F_{1}( set ) -> Element of REAL , F_{2}( set ) -> Element of REAL , F_{3}( set ) -> Element of REAL , F_{4}( set ) -> Element of REAL , F_{5}( set ) -> Element of REAL } :

ExRealSeq5{ F

ex s being Real_Sequence st

for n being Element of NAT holds

( s . (5 * n) = F_{1}(n) & s . ((5 * n) + 1) = F_{2}(n) & s . ((5 * n) + 2) = F_{3}(n) & s . ((5 * n) + 3) = F_{4}(n) & s . ((5 * n) + 4) = F_{5}(n) )

for n being Element of NAT holds

( s . (5 * n) = F

proof end;

scheme :: SCHEME1:sch 6

PartFuncExD2{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object ], P_{2}[ object ], F_{3}( object ) -> Element of F_{2}(), F_{4}( object ) -> Element of F_{2}() } :

PartFuncExD2{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or P_{2}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) ) ) )

provided
( ( for c being Element of F

( c in dom f iff ( P

( ( P

proof end;

scheme :: SCHEME1:sch 7

PartFuncExD29{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object ], P_{2}[ object ], F_{3}( object ) -> Element of F_{2}(), F_{4}( object ) -> Element of F_{2}() } :

PartFuncExD29{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or P_{2}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) ) ) )

provided
( ( for c being Element of F

( c in dom f iff ( P

( ( P

proof end;

scheme :: SCHEME1:sch 8

PartFuncExD299{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set ], F_{3}( set ) -> Element of F_{2}(), F_{4}( set ) -> Element of F_{2}() } :

PartFuncExD299{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( f is total & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{1}[c] implies f . c = F_{4}(c) ) ) ) )

( f is total & ( for c being Element of F

( ( P

proof end;

scheme :: SCHEME1:sch 9

PartFuncExD3{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object ], P_{2}[ object ], P_{3}[ object ], F_{3}( object ) -> Element of F_{2}(), F_{4}( object ) -> Element of F_{2}(), F_{5}( object ) -> Element of F_{2}() } :

PartFuncExD3{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or P_{2}[c] or P_{3}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) & ( P_{3}[c] implies f . c = F_{5}(c) ) ) ) )

provided( ( for c being Element of F

( c in dom f iff ( P

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) )

( ( P

proof end;

scheme :: SCHEME1:sch 10

PartFuncExD39{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object ], P_{2}[ object ], P_{3}[ object ], F_{3}( object ) -> Element of F_{2}(), F_{4}( object ) -> Element of F_{2}(), F_{5}( object ) -> Element of F_{2}() } :

PartFuncExD39{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or P_{2}[c] or P_{3}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) & ( P_{3}[c] implies f . c = F_{5}(c) ) ) ) )

provided( ( for c being Element of F

( c in dom f iff ( P

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] & P_{2}[c] implies F_{3}(c) = F_{4}(c) ) & ( P_{1}[c] & P_{3}[c] implies F_{3}(c) = F_{5}(c) ) & ( P_{2}[c] & P_{3}[c] implies F_{4}(c) = F_{5}(c) ) )

( ( P

proof end;

scheme :: SCHEME1:sch 11

PartFuncExD4{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object ], P_{2}[ object ], P_{3}[ object ], P_{4}[ object ], F_{3}( object ) -> Element of F_{2}(), F_{4}( object ) -> Element of F_{2}(), F_{5}( object ) -> Element of F_{2}(), F_{6}( object ) -> Element of F_{2}() } :

PartFuncExD4{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for c being Element of F_{1}() holds

( c in dom f iff ( P_{1}[c] or P_{2}[c] or P_{3}[c] or P_{4}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom f holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) & ( P_{3}[c] implies f . c = F_{5}(c) ) & ( P_{4}[c] implies f . c = F_{6}(c) ) ) ) )

provided( ( for c being Element of F

( c in dom f iff ( P

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{1}[c] implies not P_{4}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{4}[c] ) & ( P_{3}[c] implies not P_{4}[c] ) )

( ( P

proof end;

scheme :: SCHEME1:sch 12

PartFuncExS2{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object ], P_{2}[ object ], F_{3}( object ) -> set , F_{4}( object ) -> set } :

PartFuncExS2{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] ) ) ) ) & ( for x being object st x in dom f holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) ) ) )

provided( ( for x being object holds

( x in dom f iff ( x in F

( ( P

A1:
for x being object st x in F_{1}() & P_{1}[x] holds

not P_{2}[x]
and

A2: for x being object st x in F_{1}() & P_{1}[x] holds

F_{3}(x) in F_{2}()
and

A3: for x being object st x in F_{1}() & P_{2}[x] holds

F_{4}(x) in F_{2}()

not P

A2: for x being object st x in F

F

A3: for x being object st x in F

F

proof end;

scheme :: SCHEME1:sch 13

PartFuncExS3{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object ], P_{2}[ object ], P_{3}[ object ], F_{3}( object ) -> set , F_{4}( object ) -> set , F_{5}( object ) -> set } :

PartFuncExS3{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] or P_{3}[x] ) ) ) ) & ( for x being object st x in dom f holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) & ( P_{3}[x] implies f . x = F_{5}(x) ) ) ) )

provided( ( for x being object holds

( x in dom f iff ( x in F

( ( P

A1:
for x being object st x in F_{1}() holds

( ( P_{1}[x] implies not P_{2}[x] ) & ( P_{1}[x] implies not P_{3}[x] ) & ( P_{2}[x] implies not P_{3}[x] ) )
and

A2: for x being object st x in F_{1}() & P_{1}[x] holds

F_{3}(x) in F_{2}()
and

A3: for x being object st x in F_{1}() & P_{2}[x] holds

F_{4}(x) in F_{2}()
and

A4: for x being object st x in F_{1}() & P_{3}[x] holds

F_{5}(x) in F_{2}()

( ( P

A2: for x being object st x in F

F

A3: for x being object st x in F

F

A4: for x being object st x in F

F

proof end;

scheme :: SCHEME1:sch 14

PartFuncExS4{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object ], P_{2}[ object ], P_{3}[ object ], P_{4}[ object ], F_{3}( object ) -> set , F_{4}( object ) -> set , F_{5}( object ) -> set , F_{6}( object ) -> set } :

PartFuncExS4{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] or P_{3}[x] or P_{4}[x] ) ) ) ) & ( for x being object st x in dom f holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) & ( P_{3}[x] implies f . x = F_{5}(x) ) & ( P_{4}[x] implies f . x = F_{6}(x) ) ) ) )

provided( ( for x being object holds

( x in dom f iff ( x in F

( ( P

A1:
for x being object st x in F_{1}() holds

( ( P_{1}[x] implies not P_{2}[x] ) & ( P_{1}[x] implies not P_{3}[x] ) & ( P_{1}[x] implies not P_{4}[x] ) & ( P_{2}[x] implies not P_{3}[x] ) & ( P_{2}[x] implies not P_{4}[x] ) & ( P_{3}[x] implies not P_{4}[x] ) )
and

A2: for x being object st x in F_{1}() & P_{1}[x] holds

F_{3}(x) in F_{2}()
and

A3: for x being object st x in F_{1}() & P_{2}[x] holds

F_{4}(x) in F_{2}()
and

A4: for x being object st x in F_{1}() & P_{3}[x] holds

F_{5}(x) in F_{2}()
and

A5: for x being object st x in F_{1}() & P_{4}[x] holds

F_{6}(x) in F_{2}()

( ( P

A2: for x being object st x in F

F

A3: for x being object st x in F

F

A4: for x being object st x in F

F

A5: for x being object st x in F

F

proof end;

scheme :: SCHEME1:sch 15

PartFuncExCD2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ set , set ], P_{2}[ set , set ], F_{4}( set , set ) -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}() } :

PartFuncExCD2{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] ) ) ) & ( for c being Element of F_{1}()

for d being Element of F_{2}() st [c,d] in dom f holds

( ( P_{1}[c,d] implies f . [c,d] = F_{4}(c,d) ) & ( P_{2}[c,d] implies f . [c,d] = F_{5}(c,d) ) ) ) )

provided( ( for c being Element of F

for d being Element of F

( [c,d] in dom f iff ( P

for d being Element of F

( ( P

A1:
for c being Element of F_{1}()

for d being Element of F_{2}() st P_{1}[c,d] holds

not P_{2}[c,d]

for d being Element of F

not P

proof end;

scheme :: SCHEME1:sch 16

PartFuncExCD3{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ set , set ], P_{2}[ set , set ], P_{3}[ set , set ], F_{4}( set , set ) -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}(), F_{6}( set , set ) -> Element of F_{3}() } :

PartFuncExCD3{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) ) ) & ( for c being Element of F_{1}()

for r being Element of F_{2}() st [c,r] in dom f holds

( ( P_{1}[c,r] implies f . [c,r] = F_{4}(c,r) ) & ( P_{2}[c,r] implies f . [c,r] = F_{5}(c,r) ) & ( P_{3}[c,r] implies f . [c,r] = F_{6}(c,r) ) ) ) )

provided( ( for c being Element of F

for d being Element of F

( [c,d] in dom f iff ( P

for r being Element of F

( ( P

A1:
for c being Element of F_{1}()

for s being Element of F_{2}() holds

( ( P_{1}[c,s] implies not P_{2}[c,s] ) & ( P_{1}[c,s] implies not P_{3}[c,s] ) & ( P_{2}[c,s] implies not P_{3}[c,s] ) )

for s being Element of F

( ( P

proof end;

scheme :: SCHEME1:sch 17

PartFuncExCS2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , P_{1}[ object , object ], P_{2}[ object , object ], F_{4}( object , object ) -> object , F_{5}( object , object ) -> object } :

PartFuncExCS2{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] ) ) ) ) & ( for x, y being object st [x,y] in dom f holds

( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) ) ) )

provided( ( for x, y being object holds

( [x,y] in dom f iff ( x in F

( ( P

A1:
for x, y being object st x in F_{1}() & y in F_{2}() & P_{1}[x,y] holds

not P_{2}[x,y]
and

A2: for x, y being object st x in F_{1}() & y in F_{2}() & P_{1}[x,y] holds

F_{4}(x,y) in F_{3}()
and

A3: for x, y being object st x in F_{1}() & y in F_{2}() & P_{2}[x,y] holds

F_{5}(x,y) in F_{3}()

not P

A2: for x, y being object st x in F

F

A3: for x, y being object st x in F

F

proof end;

scheme :: SCHEME1:sch 18

PartFuncExCS3{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , P_{1}[ object , object ], P_{2}[ object , object ], P_{3}[ object , object ], F_{4}( object , object ) -> object , F_{5}( object , object ) -> object , F_{6}( object , object ) -> object } :

PartFuncExCS3{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] or P_{3}[x,y] ) ) ) ) & ( for x, y being object st [x,y] in dom f holds

( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(x,y) ) ) ) )

provided( ( for x, y being object holds

( [x,y] in dom f iff ( x in F

( ( P

A1:
for x, y being object st x in F_{1}() & y in F_{2}() holds

( ( P_{1}[x,y] implies not P_{2}[x,y] ) & ( P_{1}[x,y] implies not P_{3}[x,y] ) & ( P_{2}[x,y] implies not P_{3}[x,y] ) )
and

A2: for x, y being object st x in F_{1}() & y in F_{2}() & P_{1}[x,y] holds

F_{4}(x,y) in F_{3}()
and

A3: for x, y being object st x in F_{1}() & y in F_{2}() & P_{2}[x,y] holds

F_{5}(x,y) in F_{3}()
and

A4: for x, y being object st x in F_{1}() & y in F_{2}() & P_{3}[x,y] holds

F_{6}(x,y) in F_{3}()

( ( P

A2: for x, y being object st x in F

F

A3: for x, y being object st x in F

F

A4: for x, y being object st x in F

F

proof end;

scheme :: SCHEME1:sch 19

ExFuncD3{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set ], P_{2}[ set ], P_{3}[ set ], F_{3}( set ) -> Element of F_{2}(), F_{4}( set ) -> Element of F_{2}(), F_{5}( set ) -> Element of F_{2}() } :

ExFuncD3{ F

ex f being Function of F_{1}(),F_{2}() st

for c being Element of F_{1}() holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) & ( P_{3}[c] implies f . c = F_{5}(c) ) )

providedfor c being Element of F

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) )
and

A2: for c being Element of F_{1}() holds

( P_{1}[c] or P_{2}[c] or P_{3}[c] )

( ( P

A2: for c being Element of F

( P

proof end;

scheme :: SCHEME1:sch 20

ExFuncD4{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set ], P_{2}[ set ], P_{3}[ set ], P_{4}[ set ], F_{3}( set ) -> Element of F_{2}(), F_{4}( set ) -> Element of F_{2}(), F_{5}( set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}() } :

ExFuncD4{ F

ex f being Function of F_{1}(),F_{2}() st

for c being Element of F_{1}() holds

( ( P_{1}[c] implies f . c = F_{3}(c) ) & ( P_{2}[c] implies f . c = F_{4}(c) ) & ( P_{3}[c] implies f . c = F_{5}(c) ) & ( P_{4}[c] implies f . c = F_{6}(c) ) )

providedfor c being Element of F

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{1}[c] implies not P_{4}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{4}[c] ) & ( P_{3}[c] implies not P_{4}[c] ) )
and

A2: for c being Element of F_{1}() holds

( P_{1}[c] or P_{2}[c] or P_{3}[c] or P_{4}[c] )

( ( P

A2: for c being Element of F

( P

proof end;

scheme :: SCHEME1:sch 21

FuncExCD2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ set , set ], F_{4}( set , set ) -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}() } :

FuncExCD2{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for c being Element of F_{1}()

for d being Element of F_{2}() st [c,d] in dom f holds

( ( P_{1}[c,d] implies f . [c,d] = F_{4}(c,d) ) & ( P_{1}[c,d] implies f . [c,d] = F_{5}(c,d) ) )

for c being Element of F

for d being Element of F

( ( P

proof end;

scheme :: SCHEME1:sch 22

FuncExCD3{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ set , set ], P_{2}[ set , set ], P_{3}[ set , set ], F_{4}( set , set ) -> Element of F_{3}(), F_{5}( set , set ) -> Element of F_{3}(), F_{6}( set , set ) -> Element of F_{3}() } :

FuncExCD3{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) ) ) & ( for c being Element of F_{1}()

for d being Element of F_{2}() st [c,d] in dom f holds

( ( P_{1}[c,d] implies f . [c,d] = F_{4}(c,d) ) & ( P_{2}[c,d] implies f . [c,d] = F_{5}(c,d) ) & ( P_{3}[c,d] implies f . [c,d] = F_{6}(c,d) ) ) ) )

provided( ( for c being Element of F

for d being Element of F

( [c,d] in dom f iff ( P

for d being Element of F

( ( P

A1:
for c being Element of F_{1}()

for d being Element of F_{2}() holds

( ( P_{1}[c,d] implies not P_{2}[c,d] ) & ( P_{1}[c,d] implies not P_{3}[c,d] ) & ( P_{2}[c,d] implies not P_{3}[c,d] ) )
and

A2: for c being Element of F_{1}()

for d being Element of F_{2}() holds

( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] )

for d being Element of F

( ( P

A2: for c being Element of F

for d being Element of F

( P

proof end;