let IT, IT9 be Subset of bound_QC-variables ; :: thesis: ( ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( IT = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( 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 ,(bool bound_QC-variables ) st
( IT9 = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( 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 ,(bool bound_QC-variables ) such that A2: IT = F1 . p and
A3: for p being Element of QC-WFF holds
( F1 . VERUM = {} & ( p is atomic implies F1 . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( 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 ,(bool bound_QC-variables ) holds
( not IT9 = F . p or ex p being Element of QC-WFF st
( F . VERUM = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( 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 ,(bool bound_QC-variables ) such that A4: IT9 = F2 . p and
A5: for p being Element of QC-WFF holds
( F2 . VERUM = {} & ( p is atomic implies F2 . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( 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 ] means F1 . $1 = F2 . $1;
A6: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds S₁[P ! ll]

proof

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

end;

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

proof

let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A10: F1 . p = F2 . p ; :: thesis: S₁[ 'not' p]
A11: 'not' p is negative by Def18;
then A12: the_argument_of ('not' p) = p by Def23;
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
for p being Element of QC-WFF st S₁[p] holds
S₁[ All x,p]

proof

let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st S₁[p] holds
S₁[ All x,p]
let p be Element of QC-WFF ; :: 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 by Def20;
then A16: ( the_scope_of (All x,p) = p & bound_in (All x,p) = x ) by Def26, Def27;
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 st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF ; :: 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 by Def19;
then A20: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by Def24, Def25;
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 ] by A3, A5;
for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 1(A6, A21, A9, A17, A13);
hence IT = IT9 by A2, A4; :: thesis: verum