let A be preIfWhileAlgebra; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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; :: according to AOFA_000:def 28 :: thesis: ( 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 :: according to AOFA_000:def 29 :: thesis: ( 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; :: thesis: 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; :: thesis: (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 ; :: thesis: verum

end;

hereby :: according to AOFA_000:def 30 :: thesis: pr1 (S, the carrier of A) complies_with_while_wrt T

let s be Element of S; :: thesis: 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; :: thesis: ( ( (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; :: thesis: verum

end;

let s be Element of S; :: according to AOFA_000:def 31 :: thesis: 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; :: thesis: ( ( (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; :: thesis: verum