let f1 be FinSequence of B; :: thesis: ( f1 = pr2 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) )
hereby :: thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) implies f1 = pr2 h1 )
assume A3: f1 = pr2 h1 ; :: thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) )
then A4: dom f1 = dom h1 by MCART_1:def 13;
hence len f1 = len h1 by FINSEQ_3:29; :: thesis: for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2
let n be Nat; :: thesis: ( n in dom f1 implies f1 . n = (h1 . n) `2 )
thus ( n in dom f1 implies f1 . n = (h1 . n) `2 ) by A3, A4, MCART_1:def 13; :: thesis: verum
end;
assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) ; :: thesis: f1 = pr2 h1
then ( dom f1 = dom h1 & ( for n being object st n in dom f1 holds
f1 . n = (h1 . n) `2 ) ) by FINSEQ_3:29;
hence f1 = pr2 h1 by MCART_1:def 13; :: thesis: verum