let a, b, c be object ; :: 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_1:45, FINSEQ_3:1 ;
A2: dom ((1,2,3) --> (a,b,c)) = {1,2,3} by FUNCT_4:128;

now :: thesis: for x being object 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 object ; :: 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 FUNCT_4:134
.= <*a,b,c*> . x by A4 ;
:: 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 FUNCT_4:135
.= <*a,b,c*> . x by A5 ;
:: 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 FUNCT_4:135
.= <*a,b,c*> . x by A6 ;
:: thesis: verum

end;

end;

end;

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