let A be preIfWhileAlgebra; for S being non empty set
for T being Subset of S holds
( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
let S be non empty set ; for T being Subset of S holds
( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
let T be Subset of S; ( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
set f = pr1 (S, the carrier of A);
thus
for s being Element of S holds (pr1 (S, the carrier of A)) . (s,(EmptyIns A)) = s
by FUNCT_3:def 4; AOFA_000:def 28 ( pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
hereby AOFA_000:def 29 ( pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
let s be
Element of
S;
for I1, I2 being Element of A holds (pr1 (S, the carrier of A)) . (s,(I1 \; I2)) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,I1)),I2)let I1,
I2 be
Element of
A;
(pr1 (S, the carrier of A)) . (s,(I1 \; I2)) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,I1)),I2)thus (pr1 (S, the carrier of A)) . (
s,
(I1 \; I2)) =
s
by FUNCT_3:def 4
.=
(pr1 (S, the carrier of A)) . (
s,
I1)
by FUNCT_3:def 4
.=
(pr1 (S, the carrier of A)) . (
((pr1 (S, the carrier of A)) . (s,I1)),
I2)
by FUNCT_3:def 4
;
verum
end;
hereby AOFA_000:def 30 pr1 (S, the carrier of A) complies_with_while_wrt T
let s be
Element of
S;
for C, I1, I2 being Element of A holds
( ( (pr1 (S, the carrier of A)) . (s,C) in T implies (pr1 (S, the carrier of A)) . (s,(if-then-else (C,I1,I2))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I1) ) & ( (pr1 (S, the carrier of A)) . (s,C) nin T implies (pr1 (S, the carrier of A)) . (s,(if-then-else (C,I1,I2))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I2) ) )let C,
I1,
I2 be
Element of
A;
( ( (pr1 (S, the carrier of A)) . (s,C) in T implies (pr1 (S, the carrier of A)) . (s,(if-then-else (C,I1,I2))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I1) ) & ( (pr1 (S, the carrier of A)) . (s,C) nin T implies (pr1 (S, the carrier of A)) . (s,(if-then-else (C,I1,I2))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I2) ) )(pr1 (S, the carrier of A)) . (
s,
(if-then-else (C,I1,I2))) =
s
by FUNCT_3:def 4
.=
(pr1 (S, the carrier of A)) . (
s,
C)
by FUNCT_3:def 4
;
hence
( (
(pr1 (S, the carrier of A)) . (
s,
C)
in T implies
(pr1 (S, the carrier of A)) . (
s,
(if-then-else (C,I1,I2)))
= (pr1 (S, the carrier of A)) . (
((pr1 (S, the carrier of A)) . (s,C)),
I1) ) & (
(pr1 (S, the carrier of A)) . (
s,
C)
nin T implies
(pr1 (S, the carrier of A)) . (
s,
(if-then-else (C,I1,I2)))
= (pr1 (S, the carrier of A)) . (
((pr1 (S, the carrier of A)) . (s,C)),
I2) ) )
by FUNCT_3:def 4;
verum
end;
let s be Element of S; AOFA_000:def 31 for C, I being Element of A holds
( ( (pr1 (S, the carrier of A)) . (s,C) in T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I)),(while (C,I))) ) & ( (pr1 (S, the carrier of A)) . (s,C) nin T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (s,C) ) )
let C, I be Element of A; ( ( (pr1 (S, the carrier of A)) . (s,C) in T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I)),(while (C,I))) ) & ( (pr1 (S, the carrier of A)) . (s,C) nin T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (s,C) ) )
(pr1 (S, the carrier of A)) . (s,C) = s
by FUNCT_3:def 4;
hence
( ( (pr1 (S, the carrier of A)) . (s,C) in T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (((pr1 (S, the carrier of A)) . (s,C)),I)),(while (C,I))) ) & ( (pr1 (S, the carrier of A)) . (s,C) nin T implies (pr1 (S, the carrier of A)) . (s,(while (C,I))) = (pr1 (S, the carrier of A)) . (s,C) ) )
by FUNCT_3:def 4; verum