let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for Y, X 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 Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds
Y common_on_dom H
let Y, X 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

let n be Element of NAT ; :: thesis: Y c= dom (H . n)
X c= dom (H . n) by A3, Def10;
hence Y c= dom (H . n) by A1, XBOOLE_1:1; :: thesis: verum

end;

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