thus ex d being Element of F₁() ex F being Function of QC-WFF,F₁() st
( d = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() st
( x1 = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() st
( x2 = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() such that
A1: ( F . VERUM = F₂() & ( for p being Element of QC-WFF 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₁() st
( F . F₃() = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() st
( x1 = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() st
( x2 = F . F₃() & ( for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() such that A2: x1 = F1 . F₃() and
A3: for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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₁() holds
( not x2 = F . F₃() or ex p being Element of QC-WFF ex d1, d2 being Element of F₁() st
( ( p = VERUM 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₁() such that A4: x2 = F2 . F₃() and
A5: for p being Element of QC-WFF
for d1, d2 being Element of F₁() holds
( ( p = VERUM 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