let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for U being Subset of (P *)
for n being Nat
for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds
p ^ q in Polish-expression-layer (P,A,U)
let A be Function of P,NAT; :: thesis: for U being Subset of (P *)
for n being Nat
for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds
p ^ q in Polish-expression-layer (P,A,U)
let U be Subset of (P *); :: thesis: for n being Nat
for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds
p ^ q in Polish-expression-layer (P,A,U)
let n be Nat; :: thesis: for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds
p ^ q in Polish-expression-layer (P,A,U)
let p, q be FinSequence; :: thesis: ( p in P & n = A . p & q in U ^^ n implies p ^ q in Polish-expression-layer (P,A,U) )
set r = p ^ q;
assume that
A1: p in P and
A2: n = A . p and
A3: q in U ^^ n ; :: thesis: p ^ q in Polish-expression-layer (P,A,U)
A4: q in P * by A3, Th14, TARSKI:def 3;
p in P * by A1, Th9, TARSKI:def 3;
then p ^ q in P * by A4, Th12;
hence p ^ q in Polish-expression-layer (P,A,U) by A1, A2, A3, Def6; :: thesis: verum