ex M being non empty strict MonoidalSubStr of F₁() st
for x being Element of F₁() holds
( x in the carrier of M iff P₁[x] )

A1: for x, y being Element of F₁() st P₁[x] & P₁[y] holds
P₁[x * y] and
A2: P₁[ 1. F₁()]