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 A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_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 (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) )

assume A1: for n being Nat holds A3 . n = (A1 . n) /\ (A2 . n) ; :: thesis: for n being Nat holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)

let n be Nat; :: thesis: (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)

reconsider X3 = inferior_setsequence A3 as SetSequence of X ;

reconsider X2 = inferior_setsequence A2 as SetSequence of X ;

set B = A1;

reconsider X1 = inferior_setsequence A1 as SetSequence of X ;

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

for n being Nat holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_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 (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) )

assume A1: for n being Nat holds A3 . n = (A1 . n) /\ (A2 . n) ; :: thesis: for n being Nat holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)

let n be Nat; :: thesis: (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)

reconsider X3 = inferior_setsequence A3 as SetSequence of X ;

reconsider X2 = inferior_setsequence A2 as SetSequence of X ;

set B = A1;

reconsider X1 = inferior_setsequence A1 as SetSequence of X ;

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

proof

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

assume x in (X1 . n) /\ (X2 . n) ; :: thesis: x in X3 . n

then A3: ( x in X1 . n & x in X2 . n ) by XBOOLE_0:def 4;

end;assume x in (X1 . n) /\ (X2 . n) ; :: thesis: x in X3 . n

then A3: ( x in X1 . n & x in X2 . n ) by XBOOLE_0:def 4;

now :: thesis: for k being Nat holds x in A3 . (n + k)

hence
x in X3 . n
by Th19; :: thesis: verumlet k be Nat; :: thesis: x in A3 . (n + k)

( x in A1 . (n + k) & x in A2 . (n + k) ) by A3, Th19;

then x in (A1 . (n + k)) /\ (A2 . (n + k)) by XBOOLE_0:def 4;

hence x in A3 . (n + k) by A1; :: thesis: verum

end;( x in A1 . (n + k) & x in A2 . (n + k) ) by A3, Th19;

then x in (A1 . (n + k)) /\ (A2 . (n + k)) by XBOOLE_0:def 4;

hence x in A3 . (n + k) by A1; :: thesis: verum

proof

hence
(inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
by A2, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X3 . n or x in (X1 . n) /\ (X2 . n) )

assume A4: x in X3 . n ; :: thesis: x in (X1 . n) /\ (X2 . n)

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

end;assume A4: x in X3 . n ; :: thesis: x in (X1 . n) /\ (X2 . n)

now :: thesis: for k being Nat holds

( x in A1 . (n + k) & x in A2 . (n + k) )

then
( x in X1 . n & x in X2 . n )
by Th19;( x in A1 . (n + k) & x in A2 . (n + k) )

let k be Nat; :: thesis: ( x in A1 . (n + k) & x in A2 . (n + k) )

x in A3 . (n + k) by A4, Th19;

then x in (A1 . (n + k)) /\ (A2 . (n + k)) by A1;

hence ( x in A1 . (n + k) & x in A2 . (n + k) ) by XBOOLE_0:def 4; :: thesis: verum

end;x in A3 . (n + k) by A4, Th19;

then x in (A1 . (n + k)) /\ (A2 . (n + k)) by A1;

hence ( x in A1 . (n + k) & x in A2 . (n + k) ) by XBOOLE_0:def 4; :: thesis: verum

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