let D be non empty set ; :: thesis: for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & X common_on_dom H holds
Z common_on_dom H
let Z be set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & X common_on_dom H holds
Z common_on_dom H
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & X common_on_dom H holds
Z common_on_dom H
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st Z c= X & Z <> {} & X common_on_dom H holds
Z common_on_dom H
let X be set ; :: thesis: ( Z c= X & Z <> {} & X common_on_dom H implies Z common_on_dom H )
assume that
A1: Z c= X and
A2: Z <> {} and
A3: X common_on_dom H ; :: thesis: Z common_on_dom H

now :: thesis: for n being Nat holds Z c= dom (H . n)

let n be Nat; :: thesis: Z c= dom (H . n)
X c= dom (H . n) by A3;
hence Z c= dom (H . n) by A1; :: thesis: verum

end;

hence Z common_on_dom H by A2; :: thesis: verum