thus
ex d being Element of F2() ex F being Function of (QC-WFF F1()),F2() st
( d = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) )
for x1, x2 being Element of F2() st ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) holds
x1 = x2proof
consider F being
Function of
(QC-WFF F1()),
F2()
such that A1:
(
F . (VERUM F1()) = F3() & ( for
p being
Element of
QC-WFF F1() holds
( (
p is
atomic implies
F . p = F5(
p) ) & (
p is
negative implies
F . p = F6(
(F . (the_argument_of p))) ) & (
p is
conjunctive implies
F . p = F7(
(F . (the_left_argument_of p)),
(F . (the_right_argument_of p))) ) & (
p is
universal implies
F . p = F8(
p,
(F . (the_scope_of p))) ) ) ) )
from QC_LANG1:sch 3();
take
F . F4()
;
ex F being Function of (QC-WFF F1()),F2() st
( F . F4() = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) )
take
F
;
( F . F4() = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) )
thus
(
F . F4()
= F . F4() & ( for
p being
Element of
QC-WFF F1()
for
d1,
d2 being
Element of
F2() holds
( (
p = VERUM F1() implies
F . p = F3() ) & (
p is
atomic implies
F . p = F5(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = F6(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = F7(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = F8(
p,
d1) ) ) ) )
by A1;
verum
end;
let x1, x2 be Element of F2(); ( ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) implies x1 = x2 )
given F1 being Function of (QC-WFF F1()),F2() such that A2:
x1 = F1 . F4()
and
A3:
for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F1 . p = F3() ) & ( p is atomic implies F1 . p = F5(p) ) & ( p is negative & d1 = F1 . (the_argument_of p) implies F1 . p = F6(d1) ) & ( p is conjunctive & d1 = F1 . (the_left_argument_of p) & d2 = F1 . (the_right_argument_of p) implies F1 . p = F7(d1,d2) ) & ( p is universal & d1 = F1 . (the_scope_of p) implies F1 . p = F8(p,d1) ) )
; ( for F being Function of (QC-WFF F1()),F2() holds
( not x2 = F . F4() or ex p being Element of QC-WFF F1() ex d1, d2 being Element of F2() st
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) implies ( p is universal & d1 = F . (the_scope_of p) & not F . p = F8(p,d1) ) ) ) or x1 = x2 )
given F2 being Function of (QC-WFF F1()),F2() such that A4:
x2 = F2 . F4()
and
A5:
for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F2 . p = F3() ) & ( p is atomic implies F2 . p = F5(p) ) & ( p is negative & d1 = F2 . (the_argument_of p) implies F2 . p = F6(d1) ) & ( p is conjunctive & d1 = F2 . (the_left_argument_of p) & d2 = F2 . (the_right_argument_of p) implies F2 . p = F7(d1,d2) ) & ( p is universal & d1 = F2 . (the_scope_of p) implies F2 . p = F8(p,d1) ) )
; x1 = x2
F1 = F2
from QC_LANG3:sch 1(A3, A5);
hence
x1 = x2
by A2, A4; verum