let A be QC-alphabet ; for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
let x be bound_QC-variable of A; for p being Element of QC-WFF A st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
let p be Element of QC-WFF A; ( p is conjunctive implies p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) )
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1:
p . x = F . p
and
A2:
for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) )
by Def3;
consider F2 being Function of (QC-WFF A),(QC-WFF A) such that
A3:
(the_right_argument_of p) . x = F2 . (the_right_argument_of p)
and
A4:
for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) )
by Def3;
A5:
F2 = F
by A2, A4, Lm2;
consider F1 being Function of (QC-WFF A),(QC-WFF A) such that
A6:
(the_left_argument_of p) . x = F1 . (the_left_argument_of p)
and
A7:
for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) )
by Def3;
F1 = F
by A2, A7, Lm2;
hence
( p is conjunctive implies p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) )
by A1, A2, A6, A3, A5; verum