let IT, IT9 be Subset of (bound_QC-variables A); :: thesis: ( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( IT = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( IT9 = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) implies IT = IT9 )
given F1 being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2: IT = F1 . p and
A3: for p being Element of QC-WFF A holds
( F1 . (VERUM A) = {} & ( p is atomic implies F1 . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F1 . p = F1 . (the_argument_of p) ) & ( p is conjunctive implies F1 . p = (F1 . (the_left_argument_of p)) \/ (F1 . (the_right_argument_of p)) ) & ( p is universal implies F1 . p = (F1 . (the_scope_of p)) \ {(bound_in p)} ) ) ; :: thesis: ( for F being Function of (QC-WFF A),(bool (bound_QC-variables A)) holds
( not IT9 = F . p or ex p being Element of QC-WFF A st
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) implies ( p is universal & not F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) or IT = IT9 )
given F2 being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A4: IT9 = F2 . p and
A5: for p being Element of QC-WFF A holds
( F2 . (VERUM A) = {} & ( p is atomic implies F2 . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F2 . p = F2 . (the_argument_of p) ) & ( p is conjunctive implies F2 . p = (F2 . (the_left_argument_of p)) \/ (F2 . (the_right_argument_of p)) ) & ( p is universal implies F2 . p = (F2 . (the_scope_of p)) \ {(bound_in p)} ) ) ; :: thesis: IT = IT9
defpred S₁[ Element of QC-WFF A] means F1 . $1 = F2 . $1;
A6: for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S₁[P ! ll]

proof

let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S₁[P ! ll]
let P be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds S₁[P ! ll]
let ll be QC-variable_list of k,A; :: thesis: S₁[P ! ll]
A7: P ! ll is atomic ;
then A8: the_arguments_of (P ! ll) = ll by Def23;
hence F1 . (P ! ll) = { (ll . j) where j is Nat : ( 1 <= j & j <= len ll & ll . j in bound_QC-variables A ) } by A3, A7
.= F2 . (P ! ll) by A5, A7, A8 ;
:: thesis: verum

end;

A9: for p being Element of QC-WFF A st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of QC-WFF A; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A10: F1 . p = F2 . p ; :: thesis: S₁[ 'not' p]
A11: 'not' p is negative ;
then A12: the_argument_of ('not' p) = p by Def24;
hence F1 . ('not' p) = F2 . p by A3, A10, A11
.= F2 . ('not' p) by A5, A11, A12 ;
:: thesis: verum

end;

A13: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S₁[p] holds
S₁[ All (x,p)]

proof

let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st S₁[p] holds
S₁[ All (x,p)]
let p be Element of QC-WFF A; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume A14: F1 . p = F2 . p ; :: thesis: S₁[ All (x,p)]
A15: All (x,p) is universal ;
then A16: ( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x ) by Def27, Def28;
hence F1 . (All (x,p)) = (F2 . p) \ {x} by A3, A14, A15
.= F2 . (All (x,p)) by A5, A15, A16 ;
:: thesis: verum

end;

A17: for p, q being Element of QC-WFF A st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF A; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A18: ( F1 . p = F2 . p & F1 . q = F2 . q ) ; :: thesis: S₁[p '&' q]
A19: p '&' q is conjunctive ;
then A20: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by Def25, Def26;
hence F1 . (p '&' q) = (F2 . p) \/ (F2 . q) by A3, A18, A19
.= F2 . (p '&' q) by A5, A19, A20 ;
:: thesis: verum

end;

A21: S₁[ VERUM A] by A3, A5;
for p being Element of QC-WFF A holds S₁[p] from QC_LANG1:sch 1(A6, A21, A9, A17, A13);
hence IT = IT9 by A2, A4; :: thesis: verum