reconsider T1 = F₁() as non empty 1-sorted ;
reconsider S1 = F₂() as sequence of T1 ;
A2: ex n being Element of NAT st
for m being Element of NAT
for x being Point of T1 st n <= m & x = S1 . m holds
P₁[x] by A1;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P₁[(S1 * F₃()) . m] from FRECHET2:sch 1(A2);
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
P₁[(F₂() * F₃()) . m] ; :: thesis: verum