let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for s being Substitution of L,E
for F being Polish-WFF of L,E st s = {} holds
Subst (s,F) = F
let E be Polish-arity-function of L; :: thesis: for s being Substitution of L,E
for F being Polish-WFF of L,E st s = {} holds
Subst (s,F) = F
let s be Substitution of L,E; :: thesis: for F being Polish-WFF of L,E st s = {} holds
Subst (s,F) = F
let F be Polish-WFF of L,E; :: thesis: ( s = {} implies Subst (s,F) = F )
assume A1: s = {} ; :: thesis: Subst (s,F) = F
set W = Polish-WFF-set (L,E);
set g = Subst s;
set K = id (Polish-WFF-set (L,E));
reconsider K = id (Polish-WFF-set (L,E)) as Function ;
( dom K = Polish-WFF-set (L,E) & ( for a being object st a in Polish-WFF-set (L,E) holds
K . a in Polish-WFF-set (L,E) ) ) by FUNCT_1:17;
then reconsider K = K as Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) by FUNCT_2:3;
A2: K is Subst s -recursive

proof

let G be Polish-WFF of L,E; :: according to POLNOT_1:def 42 :: thesis: K . G = (Subst s) . [(L -head G),(K * (Polish-WFF-args G))]
set t = L -head G;
set p = Polish-WFF-args G;
set q = (L,E) -tail G;
A4: len (Polish-WFF-args G) = E . (L -head G) by Th62;
A6: not L -head G in dom s by A1;
A7: K * (Polish-WFF-args G) = Polish-WFF-args G

proof

reconsider q = K * (Polish-WFF-args G) as FinSequence of Polish-WFF-set (L,E) by FINSEQ_2:32;
A10: len (Polish-WFF-args G) = len q by FINSEQ_2:33;
A11: dom (Polish-WFF-args G) = Seg (len (Polish-WFF-args G)) by FINSEQ_1:def 3
.= dom q by A10, FINSEQ_1:def 3 ;
for k being Nat st k in dom (Polish-WFF-args G) holds
(Polish-WFF-args G) . k = q . k

proof

let k be Nat; :: thesis: ( k in dom (Polish-WFF-args G) implies (Polish-WFF-args G) . k = q . k )
assume A12: k in dom (Polish-WFF-args G) ; :: thesis: (Polish-WFF-args G) . k = q . k
rng (Polish-WFF-args G) c= Polish-WFF-set (L,E) by FINSEQ_1:def 4;
then A14: (Polish-WFF-args G) . k in Polish-WFF-set (L,E) by A12, FUNCT_1:3;
thus (Polish-WFF-args G) . k = K . ((Polish-WFF-args G) . k) by A14, FUNCT_1:17
.= q . k by A12, FUNCT_1:13 ; :: thesis: verum

end;

hence K * (Polish-WFF-args G) = Polish-WFF-args G by A11, FINSEQ_1:13; :: thesis: verum

end;

thus K . G = (L -head G) ^ ((L,E) -tail G)
.= (L -head G) ^ (FlattenSeq (Polish-WFF-args G)) by A4, Def44
.= (Subst s) . ((L -head G),(Polish-WFF-args G)) by A4, A6, Def45
.= (Subst s) . [(L -head G),(K * (Polish-WFF-args G))] by A7, BINOP_1:def 1 ; :: thesis: verum

end;

F = K . F ;
hence Subst (s,F) = F by A2, Def46; :: thesis: verum