let P be FinSequence-membered set ; :: thesis: for A being Function of P,NAT
for n being Nat
for p, q being FinSequence st p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds
(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
let A be Function of P,NAT; :: thesis: for n being Nat
for p, q being FinSequence st p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds
(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
let n be Nat; :: thesis: for p, q being FinSequence st p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds
(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
let p, q be FinSequence; :: thesis: ( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n implies (Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A) )
set U = Polish-expression-set (P,A);
assume A1: ( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n ) ; :: thesis: (Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
A2: Polish-expression-set (P,A) is A -closed ;
A3: dom A = P by FUNCT_2:def 1;
dom (Polish-operation (P,A,n,p)) = (Polish-expression-set (P,A)) ^^ n by FUNCT_2:def 1;
then (Polish-operation (P,A,n,p)) . q = p ^ q by Def12, A1;
hence (Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A) by A1, A2, A3; :: thesis: verum