let f1 be FinSequence of A; :: thesis: ( f1 = pr1 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) )

hereby :: thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) implies f1 = pr1 h1 )

assume A1: f1 = pr1 h1 ; :: thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) )
then A2: dom f1 = dom h1 by MCART_1:def 12;
hence len f1 = len h1 by FINSEQ_3:29; :: thesis: for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1
let n be Nat; :: thesis: ( n in dom f1 implies f1 . n = (h1 . n) `1 )
thus ( n in dom f1 implies f1 . n = (h1 . n) `1 ) by A1, A2, MCART_1:def 12; :: thesis: verum

end;

assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) ; :: thesis: f1 = pr1 h1
then ( dom f1 = dom h1 & ( for n being object st n in dom f1 holds
f1 . n = (h1 . n) `1 ) ) by FINSEQ_3:29;
hence f1 = pr1 h1 by MCART_1:def 12; :: thesis: verum