let f be Function of 4,REAL; ex a, b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
reconsider a = f . 0, b = f . 1, c = f . 2, d = f . 3 as Element of REAL by XREAL_0:def 1;
take
a
; ex b, c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
take
b
; ex c, d being Real st f = (0,1,2,3) --> (a,b,c,d)
take
c
; ex d being Real st f = (0,1,2,3) --> (a,b,c,d)
take
d
; f = (0,1,2,3) --> (a,b,c,d)
dom f = {0,1,2,3}
by CARD_1:52, FUNCT_2:def 1;
hence
f = (0,1,2,3) --> (a,b,c,d)
by FUNCT_4:144; verum