let X, Y, Z be set ; :: thesis: disjoin <*X,Y,Z*> = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*>
A1: len (disjoin <*X,Y,Z*>) = len <*X,Y,Z*> by Th1
.= 3 by FINSEQ_1:45 ;
then A2: len (disjoin <*X,Y,Z*>) = len <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> by FINSEQ_1:45;

now :: thesis: for k being Nat st 1 <= k & k <= len (disjoin <*X,Y,Z*>) holds
(disjoin <*X,Y,Z*>) . k = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (disjoin <*X,Y,Z*>) implies (disjoin <*X,Y,Z*>) . b₁ = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . b₁ )
assume A3: ( 1 <= k & k <= len (disjoin <*X,Y,Z*>) ) ; :: thesis: (disjoin <*X,Y,Z*>) . b₁ = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . b₁
then ( 1 <= k & k <= len <*X,Y,Z*> ) by Th1;
then A4: k in dom <*X,Y,Z*> by Th25;
not not k = 1 + 0 & ... & not k = 1 + 2 by A1, A3, NAT_1:62;

per cases then ( k = 1 or k = 2 or k = 3 ) ;

suppose A5: k = 1 ; :: thesis: (disjoin <*X,Y,Z*>) . b₁ = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . b₁

thus (disjoin <*X,Y,Z*>) . k = [:(<*X,Y,Z*> . k),{k}:] by A4, CARD_3:def 3
.= [:X,{1}:] by A5
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . k by A5 ; :: thesis: verum

end;

suppose A6: k = 2 ; :: thesis: (disjoin <*X,Y,Z*>) . b₁ = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . b₁

thus (disjoin <*X,Y,Z*>) . k = [:(<*X,Y,Z*> . k),{k}:] by A4, CARD_3:def 3
.= [:Y,{2}:] by A6
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . k by A6 ; :: thesis: verum

end;

suppose A7: k = 3 ; :: thesis: (disjoin <*X,Y,Z*>) . b₁ = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . b₁

thus (disjoin <*X,Y,Z*>) . k = [:(<*X,Y,Z*> . k),{k}:] by A4, CARD_3:def 3
.= [:Z,{3}:] by A7
.= <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> . k by A7 ; :: thesis: verum

end;

end;

end;

hence disjoin <*X,Y,Z*> = <*[:X,{1}:],[:Y,{2}:],[:Z,{3}:]*> by A2, FINSEQ_1:def 18; :: thesis: verum