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;

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

hence
x = y
by A3, A5, FINSEQ_2:9; :: thesis: verumx . 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;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