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 A1: ( Y c= X & Y <> {} & 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 A1, Def10;
hence Y c= dom (H . n) by A1, XBOOLE_1:1; :: thesis: verum

end;

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