let n be Nat; :: thesis: for c being Complex holds n |-> (c ") = (n |-> c) "
let c be Complex; :: thesis: n |-> (c ") = (n |-> c) "
set f = n |-> (c ");
set g = n |-> c;
set h = (n |-> c) " ;
A1: len (n |-> (c ")) = n ;
thus len (n |-> (c ")) = len ((n |-> c) ") by CARD_1:def 7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (n |-> (c ")) or (n |-> (c ")) . b₁ = ((n |-> c) ") . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (n |-> (c ")) or (n |-> (c ")) . k = ((n |-> c) ") . k )
assume ( 1 <= k & k <= len (n |-> (c ")) ) ; :: thesis: (n |-> (c ")) . k = ((n |-> c) ") . k
then A2: k in dom (n |-> (c ")) ;
hence (n |-> (c ")) . k = c " by A1, FINSEQ_9:20
.= ((n |-> c) . k) " by A1, A2, FINSEQ_9:20
.= ((n |-> c) ") . k by VALUED_1:10 ;
:: thesis: verum