let p be Element of HP-WFF ; :: thesis: for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)
let f be Element of dom (Subformulae p); :: thesis: (Subformulae p) | f = Subformulae ((Subformulae p) . f)
defpred S₁[ FinSequence of NAT ] means ex q being Element of HP-WFF st
( q = (Subformulae p) . $1 & (Subformulae p) | $1 = Subformulae q );
A1: for f being Element of dom (Subformulae p) st S₁[f] holds
for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S₁[f ^ <*n*>]

proof

let f be Element of dom (Subformulae p); :: thesis: ( S₁[f] implies for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S₁[f ^ <*n*>] )
given q being Element of HP-WFF such that q = (Subformulae p) . f and
A2: (Subformulae p) | f = Subformulae q ; :: thesis: for n being Element of NAT st f ^ <*n*> in dom (Subformulae p) holds
S₁[f ^ <*n*>]
let n be Element of NAT ; :: thesis: ( f ^ <*n*> in dom (Subformulae p) implies S₁[f ^ <*n*>] )
assume A3: f ^ <*n*> in dom (Subformulae p) ; :: thesis: S₁[f ^ <*n*>]
A4: (Subformulae p) | (f ^ <*n*>) = (Subformulae q) | <*n*> by A2, A3, TREES_9:3;
A5: (dom (Subformulae p)) | f = dom (Subformulae q) by A2, TREES_2:def 10;
then A6: <*n*> in dom (Subformulae q) by A3, TREES_1:def 6;
then A7: (Subformulae p) . (f ^ <*n*>) = (Subformulae q) . <*n*> by A2, A5, TREES_2:def 10;

per cases ( q is conjunctive or q is conditional or q is simple or q = VERUM ) by Th9;

suppose q is conjunctive ; :: thesis: S₁[f ^ <*n*>]

then consider r, s being Element of HP-WFF such that
A8: q = r '&' s ;
A9: Subformulae q = (r '&' s) -tree ((Subformulae r),(Subformulae s)) by A8, Th32;
then A10: dom (Subformulae q) = tree ((dom (Subformulae r)),(dom (Subformulae s))) by TREES_4:14;

now :: thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )

per cases ( n = 0 or n = 1 ) by A6, A10, Th5;

suppose A11: n = 0 ; :: thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )

take r = r; :: thesis: ( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
thus r = (Subformulae r) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A9, A11, Th7 ; :: thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae r
thus (Subformulae p) | (f ^ <*n*>) = Subformulae r by A4, A9, A11, Th8; :: thesis: verum

end;

suppose A12: n = 1 ; :: thesis: ex s being Element of HP-WFF st
( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )

take s = s; :: thesis: ( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
thus s = (Subformulae s) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A9, A12, Th7 ; :: thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae s
thus (Subformulae p) | (f ^ <*n*>) = Subformulae s by A4, A9, A12, Th8; :: thesis: verum

end;

end;

end;

hence S₁[f ^ <*n*>] ; :: thesis: verum

end;

suppose q is conditional ; :: thesis: S₁[f ^ <*n*>]

then consider r, s being Element of HP-WFF such that
A13: q = r => s ;
A14: Subformulae q = (r => s) -tree ((Subformulae r),(Subformulae s)) by A13, Th33;
then A15: dom (Subformulae q) = tree ((dom (Subformulae r)),(dom (Subformulae s))) by TREES_4:14;

now :: thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )

per cases ( n = 0 or n = 1 ) by A6, A15, Th5;

suppose A16: n = 0 ; :: thesis: ex r being Element of HP-WFF st
( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )

take r = r; :: thesis: ( r = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae r )
thus r = (Subformulae r) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A14, A16, Th7 ; :: thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae r
thus (Subformulae p) | (f ^ <*n*>) = Subformulae r by A4, A14, A16, Th8; :: thesis: verum

end;

suppose A17: n = 1 ; :: thesis: ex s being Element of HP-WFF st
( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )

take s = s; :: thesis: ( s = (Subformulae p) . (f ^ <*n*>) & (Subformulae p) | (f ^ <*n*>) = Subformulae s )
thus s = (Subformulae s) . {} by Th34
.= (Subformulae p) . (f ^ <*n*>) by A7, A14, A17, Th7 ; :: thesis: (Subformulae p) | (f ^ <*n*>) = Subformulae s
thus (Subformulae p) | (f ^ <*n*>) = Subformulae s by A4, A14, A17, Th8; :: thesis: verum

end;

end;

end;

hence S₁[f ^ <*n*>] ; :: thesis: verum

end;

suppose q is simple ; :: thesis: S₁[f ^ <*n*>]

then consider k being Element of NAT such that
A18: q = prop k ;
Subformulae q = root-tree (prop k) by A18, Def9;
then dom (Subformulae q) = {{}} by TREES_1:29, TREES_4:3;
hence S₁[f ^ <*n*>] by A6, TARSKI:def 1; :: thesis: verum

end;

suppose q = VERUM ; :: thesis: S₁[f ^ <*n*>]

then dom (Subformulae q) = {{}} by Th30, TREES_1:29, TREES_4:3;
hence S₁[f ^ <*n*>] by A6, TARSKI:def 1; :: thesis: verum

end;

end;

end;

(Subformulae p) . {} = p by Th34;
then A19: S₁[ <*> NAT] by TREES_9:1;
for f being Element of dom (Subformulae p) holds S₁[f] from HILBERT2:sch 1(A19, A1);
then S₁[f] ;
hence (Subformulae p) | f = Subformulae ((Subformulae p) . f) ; :: thesis: verum