let a, b, c, d, x, y, z, w, x', y', z', w' be set ; :: thesis: ( a,b,c,d are_mutually_different & a,b,c,d --> x,y,z,w = a,b,c,d --> x',y',z',w' implies ( x = x' & y = y' & z = z' & w = w' ) )
assume that
A1: a,b,c,d are_mutually_different and
A2: a,b,c,d --> x,y,z,w = a,b,c,d --> x',y',z',w' ; :: thesis: ( x = x' & y = y' & z = z' & w = w' )
A3: x = (a,b,c,d --> x,y,z,w) . a by A1, Th3
.= x' by A1, A2, Th3 ;
A4: y = (a,b,c,d --> x,y,z,w) . b by A1, Th3
.= y' by A1, A2, Th3 ;
A5: z = (a,b,c,d --> x,y,z,w) . c by A1, Th3
.= z' by A1, A2, Th3 ;
w = (a,b,c,d --> x,y,z,w) . d by A1, Th3
.= w' by A1, A2, Th3 ;
hence ( x = x' & y = y' & z = z' & w = w' ) by A3, A4, A5; :: thesis: verum