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

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

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

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

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

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

end;

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

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

end;

end;

end;

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