thus for g1, g2 being FinSequence of G st len g1 = len f & ( for i being Nat st i in dom f holds
g1 /. i = (f /. i) " ) & len g2 = len f & ( for j being Nat st j in dom f holds
g2 /. j = (f /. j) " ) holds
g1 = g2 :: thesis: verum
proof
let g1, g2 be FinSequence of G; :: thesis: ( len g1 = len f & ( for i being Nat st i in dom f holds
g1 /. i = (f /. i) " ) & len g2 = len f & ( for j being Nat st j in dom f holds
g2 /. j = (f /. j) " ) implies g1 = g2 )
assume that
A7: len g1 = len f and
A8: for i being Nat st i in dom f holds
g1 /. i = (f /. i) " and
A9: len g2 = len f and
A10: for j being Nat st j in dom f holds
g2 /. j = (f /. j) " ; :: thesis: g1 = g2
A11: dom g1 = dom f by A7, FINSEQ_3:29;
for k being Nat st 1 <= k & k <= len g1 holds
g1 . k = g2 . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len g1 implies g1 . k = g2 . k )
assume A12: ( 1 <= k & k <= len g1 ) ; :: thesis: g1 . k = g2 . k
k in Seg (len g2) by A7, A9, A12;
then k in dom g2 by FINSEQ_1:def 3;
then A13: g2 . k = g2 /. k by PARTFUN1:def 6;
k in Seg (len g1) by A12;
then A14: k in dom g1 by FINSEQ_1:def 3;
then ( g1 . k = g1 /. k & g1 /. k = (f /. k) " ) by A8, A11, PARTFUN1:def 6;
hence g1 . k = g2 . k by A10, A11, A14, A13; :: thesis: verum
end;
hence g1 = g2 by A7, A9; :: thesis: verum
end;