let a, b be set ; :: thesis: for c being complex number holds <*a,b,c*> = (1,2,3) --> (a,b,c)
let c be complex number ; :: thesis: <*a,b,c*> = (1,2,3) --> (a,b,c)
set f = (1,2,3) --> (a,b,c);
set g = <*a,b,c*>;
A1: dom <*a,b,c*> = Seg (len <*a,b,c*>) by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_3:1, FINSEQ_1:45 ;
A2: dom ((1,2,3) --> (a,b,c)) = {1,2,3} by BVFUNC14:11;

now :: thesis: for x being set st x in dom ((1,2,3) --> (a,b,c)) holds
((1,2,3) --> (a,b,c)) . x = <*a,b,c*> . x

let x be set ; :: thesis: ( x in dom ((1,2,3) --> (a,b,c)) implies ((1,2,3) --> (a,b,c)) . b₁ = <*a,b,c*> . b₁ )
assume A3: x in dom ((1,2,3) --> (a,b,c)) ; :: thesis: ((1,2,3) --> (a,b,c)) . b₁ = <*a,b,c*> . b₁

per cases ( x = 1 or x = 2 or x = 3 ) by A2, A3, ENUMSET1:def 1;

suppose A4: x = 1 ; :: thesis: ((1,2,3) --> (a,b,c)) . b₁ = <*a,b,c*> . b₁

hence ((1,2,3) --> (a,b,c)) . x = a by Lm6, Th28
.= <*a,b,c*> . x by A4, FINSEQ_1:45 ;
:: thesis: verum

end;

suppose A5: x = 2 ; :: thesis: ((1,2,3) --> (a,b,c)) . b₁ = <*a,b,c*> . b₁

hence ((1,2,3) --> (a,b,c)) . x = b by Lm6, Th28
.= <*a,b,c*> . x by A5, FINSEQ_1:45 ;
:: thesis: verum

end;

suppose A6: x = 3 ; :: thesis: ((1,2,3) --> (a,b,c)) . b₁ = <*a,b,c*> . b₁

hence ((1,2,3) --> (a,b,c)) . x = c by Lm6, Th28
.= <*a,b,c*> . x by A6, FINSEQ_1:45 ;
:: thesis: verum

end;

end;

end;

hence <*a,b,c*> = (1,2,3) --> (a,b,c) by A1, BVFUNC14:11, FUNCT_1:2; :: thesis: verum