let a, b, c, d be 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 aa = a, bb = b, c9 = c, d9 = d as Element of REAL by XREAL_0:def 1;
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*] = [*aa,bb*] by Lm3;
Re [*aa,bb*] = a by Lm7;
hence Rea [*a,b,c,d*] = a by A1, Def12; :: 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) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:52;
A3: not [*a,b,c,d*] in COMPLEX by A2, Th4;
f . 0 = a by A2, FUNCT_4:142;
hence Rea [*a,b,c,d*] = a by A3, Def12; :: 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*] = [*aa,bb*] by Lm3;
Im [*aa,bb*] = b by Lm7;
hence Im1 [*a,b,c,d*] = b by A4, Def13; :: 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) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:52;
A6: not [*a,b,c,d*] in COMPLEX by A5, Th4;
f . 1 = b by A5, FUNCT_4:141;
hence Im1 [*a,b,c,d*] = b by A6, Def13; :: 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*] = [*aa,bb*] by Lm3;
hence Im2 [*a,b,c,d*] = c by A7, Def14; :: 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) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:52;
A9: not [*a,b,c,d*] in COMPLEX by A8, Th4;
f . 2 = c by A8, FUNCT_4:140;
hence Im2 [*a,b,c,d*] = c by A9, Def14; :: 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*] = [*aa,bb*] by Lm3;
hence Im3 [*a,b,c,d*] = d by A10, Def15; :: 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) --> (aa,bb,c9,d9) by Def5;
then reconsider f = [*a,b,c,d*] as Function of 4,REAL by CARD_1:52;
A12: not [*a,b,c,d*] in COMPLEX by A11, Th4;
f . 3 = d by A11, FUNCT_4:139;
hence Im3 [*a,b,c,d*] = d by A12, Def15; :: thesis: verum
end;
end;