let f1, f2 be XFinSequence; :: thesis: for i being Nat st i < len f1 holds
(f1 ^ f2) . i = f1 . i
let i be Nat; :: thesis: ( i < len f1 implies (f1 ^ f2) . i = f1 . i )
assume i < len f1 ; :: thesis: (f1 ^ f2) . i = f1 . i
then i in dom f1 by NAT_1:45;
hence (f1 ^ f2) . i = f1 . i by AFINSQ_1:def 4; :: thesis: verum