thus ex d being Element of F₂() ex F being Function of (QC-WFF F₁()),F₂() st
( d = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) :: thesis: for x1, x2 being Element of F₂() st ex F being Function of (QC-WFF F₁()),F₂() st
( x1 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F₁()),F₂() st
( x2 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) holds
x1 = x2

proof

consider F being Function of (QC-WFF F₁()),F₂() such that
A1: ( F . (VERUM F₁()) = F₃() & ( for p being Element of QC-WFF F₁() holds
( ( p is atomic implies F . p = F₅(p) ) & ( p is negative implies F . p = F₆((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F₇((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F₈(p,(F . (the_scope_of p))) ) ) ) ) from QC_LANG1:sch 3();
take F . F₄() ; :: thesis: ex F being Function of (QC-WFF F₁()),F₂() st
( F . F₄() = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) )
take F ; :: thesis: ( F . F₄() = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) )
thus ( F . F₄() = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) by A1; :: thesis: verum

end;

let x1, x2 be Element of F₂(); :: thesis: ( ex F being Function of (QC-WFF F₁()),F₂() st
( x1 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F₁()),F₂() st
( x2 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) implies x1 = x2 )
given F1 being Function of (QC-WFF F₁()),F₂() such that A2: x1 = F1 . F₄() and
A3: for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F1 . p = F₃() ) & ( p is atomic implies F1 . p = F₅(p) ) & ( p is negative & d1 = F1 . (the_argument_of p) implies F1 . p = F₆(d1) ) & ( p is conjunctive & d1 = F1 . (the_left_argument_of p) & d2 = F1 . (the_right_argument_of p) implies F1 . p = F₇(d1,d2) ) & ( p is universal & d1 = F1 . (the_scope_of p) implies F1 . p = F₈(p,d1) ) ) ; :: thesis: ( for F being Function of (QC-WFF F₁()),F₂() holds
( not x2 = F . F₄() or ex p being Element of QC-WFF F₁() ex d1, d2 being Element of F₂() st
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) implies ( p is universal & d1 = F . (the_scope_of p) & not F . p = F₈(p,d1) ) ) ) or x1 = x2 )
given F2 being Function of (QC-WFF F₁()),F₂() such that A4: x2 = F2 . F₄() and
A5: for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F2 . p = F₃() ) & ( p is atomic implies F2 . p = F₅(p) ) & ( p is negative & d1 = F2 . (the_argument_of p) implies F2 . p = F₆(d1) ) & ( p is conjunctive & d1 = F2 . (the_left_argument_of p) & d2 = F2 . (the_right_argument_of p) implies F2 . p = F₇(d1,d2) ) & ( p is universal & d1 = F2 . (the_scope_of p) implies F2 . p = F₈(p,d1) ) ) ; :: thesis: x1 = x2
F1 = F2 from QC_LANG3:sch 1(A3, A5);
hence x1 = x2 by A2, A4; :: thesis: verum