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 (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . 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 (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) )
assume A1: for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ; :: thesis: for n being Nat holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let n be Nat; :: thesis: (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
reconsider X3 = superior_setsequence A3 as SetSequence of X ;
reconsider X2 = superior_setsequence A2 as SetSequence of X ;
set B = A1;
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
A2: (X1 . n) \/ (X2 . n) c= X3 . n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X1 . n) \/ (X2 . n) or x in X3 . n )
assume A3: x in (X1 . n) \/ (X2 . n) ; :: thesis: x in X3 . n

per cases ( x in X1 . n or x in X2 . n ) by A3, XBOOLE_0:def 3;

suppose x in X1 . n ; :: thesis: x in X3 . n

then consider k being Nat such that
A4: x in A1 . (n + k) by Th20;
A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1;
then x in A3 . (n + k) by A4, XBOOLE_0:def 3;
hence x in X3 . n by Th20; :: thesis: verum

end;

suppose x in X2 . n ; :: thesis: x in X3 . n

then consider k being Nat such that
A5: x in A2 . (n + k) by Th20;
A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1;
then x in A3 . (n + k) by A5, XBOOLE_0:def 3;
hence x in X3 . n by Th20; :: thesis: verum

end;

end;

end;

X3 . n c= (X1 . n) \/ (X2 . n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X3 . n or x in (X1 . n) \/ (X2 . n) )
assume x in X3 . n ; :: thesis: x in (X1 . n) \/ (X2 . n)
then consider k being Nat such that
A6: x in A3 . (n + k) by Th20;
A7: x in (A1 . (n + k)) \/ (A2 . (n + k)) by A1, A6;

now :: thesis: ( ( x in A1 . (n + k) & x in X1 . n ) or ( x in A2 . (n + k) & x in X2 . n ) )

per cases ( x in A1 . (n + k) or x in A2 . (n + k) ) by A7, XBOOLE_0:def 3;

case x in A1 . (n + k) ; :: thesis: x in X1 . n

hence x in X1 . n by Th20; :: thesis: verum

end;

case x in A2 . (n + k) ; :: thesis: x in X2 . n

hence x in X2 . n by Th20; :: thesis: verum

end;

end;

end;

hence x in (X1 . n) \/ (X2 . n) by XBOOLE_0:def 3; :: thesis: verum

end;

hence (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) by A2, XBOOLE_0:def 10; :: thesis: verum