let n be non zero Nat; :: thesis: for X, Y being n -element FinSequence st ( for i being Nat st i in Seg n holds
X . i c= Y . i ) holds
CarProduct X c= CarProduct Y
let X, Y be n -element FinSequence; :: thesis: ( ( for i being Nat st i in Seg n holds
X . i c= Y . i ) implies CarProduct X c= CarProduct Y )
assume A1: for i being Nat st i in Seg n holds
X . i c= Y . i ; :: thesis: CarProduct X c= CarProduct Y

now :: thesis: for x being object st x in CarProduct X holds
CarProduct X c= CarProduct Y

let x be object ; :: thesis: ( x in CarProduct X implies CarProduct X c= CarProduct Y )
assume x in CarProduct X ; :: thesis: CarProduct X c= CarProduct Y
then reconsider X1 = X as non-empty n -element FinSequence by Th6;
dom X = Seg (len X) by FINSEQ_1:def 3;
then A2: dom X = Seg n by CARD_1:def 7;
dom Y = Seg (len Y) by FINSEQ_1:def 3;
then A3: dom Y = Seg n by CARD_1:def 7;

now :: thesis: Y is non-empty

assume not Y is non-empty ; :: thesis: contradiction
then consider i being object such that
A4: ( i in dom Y & Y . i = {} ) ;
reconsider i = i as Nat by A4;
X1 . i c= Y . i by A1, A3, A4;
hence contradiction by A2, A3, A4; :: thesis: verum

end;

then reconsider Y1 = Y as non-empty n -element FinSequence ;
CarProduct X1 c= CarProduct Y1 by A1, MEASUR15:48;
hence CarProduct X c= CarProduct Y ; :: thesis: verum

end;

hence CarProduct X c= CarProduct Y ; :: thesis: verum