let F be non empty finite set ; for A being non-empty FinSequence of bool F
for i, j being Element of NAT
for B being Singlification of A,i
for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )
let A be non-empty FinSequence of bool F; for i, j being Element of NAT
for B being Singlification of A,i
for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )
let i, j be Element of NAT ; for B being Singlification of A,i
for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )
let B be Singlification of A,i; for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )
let C be Singlification of B,j; ( i in dom A & j in dom A & C . i <> {} & B . j <> {} implies ( C is Singlification of A,j & C is Singlification of A,i ) )
assume that
A1:
i in dom A
and
A2:
j in dom A
and
A3:
C . i <> {}
and
A4:
B . j <> {}
; ( C is Singlification of A,j & C is Singlification of A,i )
A5:
dom B = dom A
by Def6;
then A6:
C . i c= B . i
by A1, Def6;
A7:
A . i <> {}
by A1, Th2;
then
card (B . i) = 1
by A1, Def7;
then A8:
card (C . i) = 1
by A3, A6, NAT_1:25, NAT_1:43;
A9:
A . j <> {}
by A2, Th2;
A10:
C is Reduction of A
by Th22;
card (C . j) = 1
by A2, A4, A5, Def7;
hence
( C is Singlification of A,j & C is Singlification of A,i )
by A1, A2, A7, A9, A10, A8, Def7; verum