let X be set ; :: thesis: for A1, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let A1, A2, A3 be SetSequence of X; :: thesis: ( ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n )
assume A1: for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ; :: thesis: for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let n be Nat; :: thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
set X1 = inferior_setsequence A1;
set X2 = inferior_setsequence A2;
set X3 = inferior_setsequence A3;
now :: thesis: for x being object st x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) holds
x in (inferior_setsequence A3) . n
let x be object ; :: thesis: ( x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) implies b1 in (inferior_setsequence A3) . n )
assume A2: x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) ; :: thesis: b1 in (inferior_setsequence A3) . n
per cases ( x in (inferior_setsequence A1) . n or x in (inferior_setsequence A2) . n ) by A2, XBOOLE_0:def 3;
suppose A3: x in (inferior_setsequence A1) . n ; :: thesis: b1 in (inferior_setsequence A3) . n
now :: thesis: for k being Nat holds x in A3 . (n + k)
let k be Nat; :: thesis: x in A3 . (n + k)
( x in A1 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A3, Th19;
hence x in A3 . (n + k) by XBOOLE_0:def 3; :: thesis: verum
end;
hence x in (inferior_setsequence A3) . n by Th19; :: thesis: verum
end;
suppose A4: x in (inferior_setsequence A2) . n ; :: thesis: b1 in (inferior_setsequence A3) . n
now :: thesis: for k being Nat holds x in A3 . (n + k)
let k be Nat; :: thesis: x in A3 . (n + k)
( x in A2 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A4, Th19;
hence x in A3 . (n + k) by XBOOLE_0:def 3; :: thesis: verum
end;
hence x in (inferior_setsequence A3) . n by Th19; :: thesis: verum
end;
end;
end;
hence ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n ; :: thesis: verum