let X1, X2, X3, X4, Y1, Y2, Y3, Y4 be set ; ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
A1:
[:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:]
by ZFMISC_1:def 4;
assume A2:
( X1 <> {} & X2 <> {} & X3 <> {} )
; ( not X4 <> {} or not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
assume A3:
X4 <> {}
; ( not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
assume
[:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:]
; ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )
then A4:
[:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:]
by A1, ZFMISC_1:def 4;
[:X1,X2,X3:] = [:Y1,Y2,Y3:]
by A3, A4, A2, ZFMISC_1:110;
hence
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )
by A2, A3, A4, Th22, ZFMISC_1:110; verum