let X1, X2 be set ; :: thesis: for F1 being SetSequence of X1
for F2 being SetSequence of X2
for n being Nat st F1 is non-descending & F2 is non-descending holds
[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]
let F1 be SetSequence of X1; :: thesis: for F2 being SetSequence of X2
for n being Nat st F1 is non-descending & F2 is non-descending holds
[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]
let F2 be SetSequence of X2; :: thesis: for n being Nat st F1 is non-descending & F2 is non-descending holds
[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]
let n be Nat; :: thesis: ( F1 is non-descending & F2 is non-descending implies [:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):] )
assume ( F1 is non-descending & F2 is non-descending ) ; :: thesis: [:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]
then ( F1 . n c= F1 . (n + 1) & F2 . n c= F2 . (n + 1) ) by PROB_1:def 5, NAT_1:11;
hence [:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):] by ZFMISC_1:96; :: thesis: verum