set W = Polish-WFF-set (L,E);
set R = Polish-recursion-domain (E,(Polish-WFF-set (L,E)));
defpred S₁[ object , object ] means ex t being Element of L ex p being FinSequence of Polish-WFF-set (L,E) st
( $1 = [t,p] & ( t in dom s implies $2 = s . t ) & ( not t in dom s implies $2 = t ^ (FlattenSeq p) ) );
A1: for a being object st a in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) holds
ex b being object st
( b in Polish-WFF-set (L,E) & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) implies ex b being object st
( b in Polish-WFF-set (L,E) & S₁[a,b] ) )
assume a in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) ; :: thesis: ex b being object st
( b in Polish-WFF-set (L,E) & S₁[a,b] )
then consider t being Element of L, p being FinSequence of Polish-WFF-set (L,E) such that
A3: a = [t,p] and
A4: len p = E . t ;

per cases ( t in dom s or not t in dom s ) ;

suppose A10: t in dom s ; :: thesis: ex b being object st
( b in Polish-WFF-set (L,E) & S₁[a,b] )

take b = s . t; :: thesis: ( b in Polish-WFF-set (L,E) & S₁[a,b] )
thus b in Polish-WFF-set (L,E) by A10, PARTFUN1:4; :: thesis: S₁[a,b]
take t ; :: thesis: ex p being FinSequence of Polish-WFF-set (L,E) st
( a = [t,p] & ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
take p ; :: thesis: ( a = [t,p] & ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
thus a = [t,p] by A3; :: thesis: ( ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
thus ( t in dom s implies b = s . t ) ; :: thesis: ( not t in dom s implies b = t ^ (FlattenSeq p) )
thus ( not t in dom s implies b = t ^ (FlattenSeq p) ) by A10; :: thesis: verum

end;

suppose A12: not t in dom s ; :: thesis: ex b being object st
( b in Polish-WFF-set (L,E) & S₁[a,b] )

set u = FlattenSeq p;
take b = t ^ (FlattenSeq p); :: thesis: ( b in Polish-WFF-set (L,E) & S₁[a,b] )
FlattenSeq p in (Polish-WFF-set (L,E)) ^^ (E . t) by A4;
then FlattenSeq p in dom (Polish-operation (L,E,t)) by FUNCT_2:def 1;
then b = (Polish-operation (L,E,t)) . (FlattenSeq p) by Def12;
hence b in Polish-WFF-set (L,E) by A4, FUNCT_2:5; :: thesis: S₁[a,b]
take t ; :: thesis: ex p being FinSequence of Polish-WFF-set (L,E) st
( a = [t,p] & ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
take p ; :: thesis: ( a = [t,p] & ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
thus a = [t,p] by A3; :: thesis: ( ( t in dom s implies b = s . t ) & ( not t in dom s implies b = t ^ (FlattenSeq p) ) )
thus ( t in dom s implies b = s . t ) by A12; :: thesis: ( not t in dom s implies b = t ^ (FlattenSeq p) )
thus ( not t in dom s implies b = t ^ (FlattenSeq p) ) ; :: thesis: verum

end;

end;

end;

consider f being Function of (Polish-recursion-domain (E,(Polish-WFF-set (L,E)))),(Polish-WFF-set (L,E)) such that
A20: for a being object st a in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) holds
S₁[a,f . a] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) )
let t be Element of L; :: thesis: for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) )
let p be FinSequence of Polish-WFF-set (L,E); :: thesis: ( len p = E . t implies ( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) ) )
set a = [t,p];
assume len p = E . t ; :: thesis: ( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) )
then A21: [t,p] in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) ;
f . (t,p) = f . [t,p] by BINOP_1:def 1;
then consider t1 being Element of L, p1 being FinSequence of Polish-WFF-set (L,E) such that
A23: [t,p] = [t1,p1] and
A24: ( t1 in dom s implies f . (t,p) = s . t1 ) and
A25: ( not t1 in dom s implies f . (t,p) = t1 ^ (FlattenSeq p1) ) by A20, A21;
( t1 = t & p1 = p ) by A23, XTUPLE_0:1;
hence ( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) ) by A24, A25; :: thesis: verum