set W = Polish-WFF-set (T,A);
defpred S₁[ object , object , object ] means ex u, v being FinSequence st
( $1 = u & $2 = v & $3 = (Polish-operation (T,A,t)) . (u ^ v) );
A2: for a, b being object st a in Polish-WFF-set (T,A) & b in Polish-WFF-set (T,A) holds
ex c being object st
( c in Polish-WFF-set (T,A) & S₁[a,b,c] )

proof

let a, b be object ; :: thesis: ( a in Polish-WFF-set (T,A) & b in Polish-WFF-set (T,A) implies ex c being object st
( c in Polish-WFF-set (T,A) & S₁[a,b,c] ) )
assume that
A3: a in Polish-WFF-set (T,A) and
A4: b in Polish-WFF-set (T,A) ; :: thesis: ex c being object st
( c in Polish-WFF-set (T,A) & S₁[a,b,c] )
reconsider u = a as FinSequence by A3;
reconsider v = b as FinSequence by A4;
take c = (Polish-operation (T,A,t)) . (u ^ v); :: thesis: ( c in Polish-WFF-set (T,A) & S₁[a,b,c] )
(Polish-WFF-set (T,A)) ^^ 2 = (Polish-WFF-set (T,A)) ^^ (1 + 1)
.= ((Polish-WFF-set (T,A)) ^^ 1) ^ (Polish-WFF-set (T,A)) by Th6
.= (Polish-WFF-set (T,A)) ^ (Polish-WFF-set (T,A)) ;
then u ^ v in (Polish-WFF-set (T,A)) ^^ 2 by A3, A4, Def2;
hence c in Polish-WFF-set (T,A) by A1, FUNCT_2:5; :: thesis: S₁[a,b,c]
thus S₁[a,b,c] ; :: thesis: verum

end;

consider f being Function of [:(Polish-WFF-set (T,A)),(Polish-WFF-set (T,A)):],(Polish-WFF-set (T,A)) such that
A11: for a, b being object st a in Polish-WFF-set (T,A) & b in Polish-WFF-set (T,A) holds
S₁[a,b,f . (a,b)] from BINOP_1:sch 1(A2);
take f ; :: thesis: for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v)
let u, v be FinSequence; :: thesis: ( u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) implies f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) )
assume that
A12: u in Polish-WFF-set (T,A) and
A13: v in Polish-WFF-set (T,A) ; :: thesis: f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v)
S₁[u,v,f . (u,v)] by A11, A12, A13;
hence f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ; :: thesis: verum