let n be non zero Nat; :: thesis: for X being n -element FinSequence
for x being object holds
( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) )
let X be n -element FinSequence; :: thesis: for x being object holds
( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) )
let x be object ; :: thesis: ( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) )

per cases ( X is non-empty or not X is non-empty ) ;

suppose X is non-empty ; :: thesis: ( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) )

then reconsider X1 = X as non-empty n -element FinSequence ;
( x in CarProduct X1 iff ex px being n -element FinSequence st
( px in product X1 & x = PtCarProduct px ) ) by MEASUR15:6;
hence ( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) ) ; :: thesis: verum

end;

suppose not X is non-empty ; :: thesis: ( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) )

hence ( x in CarProduct X iff ex px being n -element FinSequence st
( px in product X & x = PtCarProduct px ) ) by Th6, CARD_3:9; :: thesis: verum

end;

end;