begin
Lm1:
for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
Lm2:
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
begin
begin
begin
begin
begin
begin
begin
begin
Lm3:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
begin
Lm4:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
begin
begin
begin