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

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

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

end;

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