let F be non empty finite set ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1: ( i in dom A & j in dom A & C . i <> {} & B . j <> {} ) ; :: thesis: ( C is Singlification of A,j & C is Singlification of A,i )
A2: dom B = dom A by Def6;
A3: ( A . i <> {} & A . j <> {} ) by A1, Th2;
A4: C is Reduction of A by Th22;
A5: card (C . j) = 1 by A1, A2, Def7;
A6: card (B . i) = 1 by A1, A3, Def7;
A7: card (C . i) <> 0 by A1;
C . i c= B . i by A1, A2, Def6;
then card (C . i) = 1 by A6, A7, NAT_1:26, NAT_1:44;
hence ( C is Singlification of A,j & C is Singlification of A,i ) by A1, A3, A4, A5, Def7; :: thesis: verum