let x1, x2, x3, x4, x5, x6 be object ; :: thesis: for f being Function st <%x1,x2,x3,x4,x5,x6%> c= f holds
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 )
let f be Function; :: thesis: ( <%x1,x2,x3,x4,x5,x6%> c= f implies ( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 ) )
set g = <%x1,x2,x3,x4,x5,x6%>;
dom <%x1,x2,x3,x4,x5,x6%> = {0,1,2,3,4,5} by Th6;
then A1: ( 0 in dom <%x1,x2,x3,x4,x5,x6%> & 1 in dom <%x1,x2,x3,x4,x5,x6%> & 2 in dom <%x1,x2,x3,x4,x5,x6%> & 3 in dom <%x1,x2,x3,x4,x5,x6%> & 4 in dom <%x1,x2,x3,x4,x5,x6%> & 5 in dom <%x1,x2,x3,x4,x5,x6%> ) by ENUMSET1:def 4;
( <%x1,x2,x3,x4,x5,x6%> . 0 = x1 & <%x1,x2,x3,x4,x5,x6%> . 1 = x2 & <%x1,x2,x3,x4,x5,x6%> . 2 = x3 & <%x1,x2,x3,x4,x5,x6%> . 3 = x4 & <%x1,x2,x3,x4,x5,x6%> . 4 = x5 & <%x1,x2,x3,x4,x5,x6%> . 5 = x6 ) ;
hence ( <%x1,x2,x3,x4,x5,x6%> c= f implies ( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 ) ) by A1, GRFUNC_1:2; :: thesis: verum