let x, y be PFuncFinSequence of (product (Carrier A)); :: thesis: ( len x = len (ComSign A) & ( for n being Nat st n in dom x holds
x . n = [[:(ProdOp (A,n)):]] ) & len y = len (ComSign A) & ( for n being Nat st n in dom y holds
y . n = [[:(ProdOp (A,n)):]] ) implies x = y )
assume that
A3: len x = len (ComSign A) and
A4: for n being Nat st n in dom x holds
x . n = [[:(ProdOp (A,n)):]] and
A5: len y = len (ComSign A) and
A6: for n being Nat st n in dom y holds
y . n = [[:(ProdOp (A,n)):]] ; :: thesis: x = y
A7: dom x = Seg (len (ComSign A)) by A3, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom x holds
x . n = y . n

let n be Nat; :: thesis: ( n in dom x implies x . n = y . n )
assume n in dom x ; :: thesis: x . n = y . n
then ( n in dom y & x . n = [[:(ProdOp (A,n)):]] ) by A4, A5, A7, FINSEQ_1:def 3;
hence x . n = y . n by A6; :: thesis: verum

end;

hence x = y by A3, A5, FINSEQ_2:9; :: thesis: verum