let x, y, z, t be Complex; XFS2FS <%x,y,z,t%> = <*x,y,z,t*>
reconsider x = x, y = y, z = z, t = t as Element of COMPLEX by XCMPLX_0:def 2;
A1:
( XFS2FS <%z%> = <*z*> & XFS2FS <%t%> = <*t*> )
by RVSUM_4:50;
( XFS2FS <%x%> = <*x*> & XFS2FS <%y%> = <*y*> )
by RVSUM_4:50;
then
XFS2FS (<%x%> ^ <%y%>) = <*x*> ^ <*y*>
by RVSUM_4:45;
then
XFS2FS ((<%x%> ^ <%y%>) ^ <%z%>) = (<*x*> ^ <*y*>) ^ <*z*>
by A1, RVSUM_4:45;
then
XFS2FS (((<%x%> ^ <%y%>) ^ <%z%>) ^ <%t%>) = ((<*x*> ^ <*y*>) ^ <*z*>) ^ <*t*>
by A1, RVSUM_4:45;
then
XFS2FS (((<%x%> ^ <%y%>) ^ <%z%>) ^ <%t%>) = <*x,y,z,t*>
by FINSEQ_4:74;
hence
XFS2FS <%x,y,z,t%> = <*x,y,z,t*>
by AFINSQ_1:def 14; verum