let P be FinSequence-membered set ; 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; 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; 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; ( 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 )
; (Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
A2:
Polish-expression-set (P,A) is A -closed
by TH51;
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 Def13, A1;
hence
(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)
by A1, A2; verum