let a, b, c, d be Element of REAL ; :: thesis: ( Rea [*a,b,c,d*] = a & Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of REAL ;
thus Rea [*a,b,c,d*] = a :: thesis: ( Im1 [*a,b,c,d*] = b & Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )

proof

per cases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;

suppose ( c = 0 & d = 0 ) ; :: thesis: Rea [*a,b,c,d*] = a

then A1: [*a,b,c,d*] = [*a,b*] by Lm4;
Re [*a,b*] = a by Lm8;
hence Rea [*a,b,c,d*] = a by A1, Def13; :: thesis: verum

end;

suppose ( c <> 0 or d <> 0 ) ; :: thesis: Rea [*a,b,c,d*] = a

then A2: [*a,b,c,d*] = 0 ,1,2,3 --> a9,b9,c9,d9 by Def6;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:90;
A3: not [*a,b,c,d*] in COMPLEX by A2, Th10;
f . 0 = a by A2, Lm1, Th3;
hence Rea [*a,b,c,d*] = a by A3, Def13; :: thesis: verum

end;

end;

end;

thus Im1 [*a,b,c,d*] = b :: thesis: ( Im2 [*a,b,c,d*] = c & Im3 [*a,b,c,d*] = d )

proof

per cases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;

suppose ( c = 0 & d = 0 ) ; :: thesis: Im1 [*a,b,c,d*] = b

then A4: [*a,b,c,d*] = [*a,b*] by Lm4;
Im [*a,b*] = b by Lm8;
hence Im1 [*a,b,c,d*] = b by A4, Def14; :: thesis: verum

end;

suppose ( c <> 0 or d <> 0 ) ; :: thesis: Im1 [*a,b,c,d*] = b

then A5: [*a,b,c,d*] = 0 ,1,2,3 --> a9,b9,c9,d9 by Def6;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:90;
A6: not [*a,b,c,d*] in COMPLEX by A5, Th10;
f . 1 = b by A5, Lm1, Th3;
hence Im1 [*a,b,c,d*] = b by A6, Def14; :: thesis: verum

end;

end;

end;

thus Im2 [*a,b,c,d*] = c :: thesis: Im3 [*a,b,c,d*] = d

proof

per cases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;

suppose A7: ( c = 0 & d = 0 ) ; :: thesis: Im2 [*a,b,c,d*] = c

then [*a,b,c,d*] = [*a,b*] by Lm4;
hence Im2 [*a,b,c,d*] = c by A7, Def15; :: thesis: verum

end;

suppose ( c <> 0 or d <> 0 ) ; :: thesis: Im2 [*a,b,c,d*] = c

then A8: [*a,b,c,d*] = 0 ,1,2,3 --> a9,b9,c9,d9 by Def6;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:90;
A9: not [*a,b,c,d*] in COMPLEX by A8, Th10;
f . 2 = c by A8, Lm1, Th3;
hence Im2 [*a,b,c,d*] = c by A9, Def15; :: thesis: verum

end;

end;

end;

per cases ( ( c = 0 & d = 0 ) or c <> 0 or d <> 0 ) ;

suppose A10: ( c = 0 & d = 0 ) ; :: thesis: Im3 [*a,b,c,d*] = d

then [*a,b,c,d*] = [*a,b*] by Lm4;
hence Im3 [*a,b,c,d*] = d by A10, Def16; :: thesis: verum

end;

suppose ( c <> 0 or d <> 0 ) ; :: thesis: Im3 [*a,b,c,d*] = d

then A11: [*a,b,c,d*] = 0 ,1,2,3 --> a9,b9,c9,d9 by Def6;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:90;
A12: not [*a,b,c,d*] in COMPLEX by A11, Th10;
f . 3 = d by A11, Lm1, Th3;
hence Im3 [*a,b,c,d*] = d by A12, Def16; :: thesis: verum

end;

end;